Ilya Sergey
where else to find them
website:http://ilyasergey.net
github:ilyasergey
bluesky:ilyasergey.bsky.social
linkedin:ilyasergey
speakerdeck:ilyasergey
what they talk about
all 9 in the filters
where they keep going back
- OOPSLA3 editions2023–2025
- ICFP2 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
all 11 in the filters
on a stage with
all 31 in the filters
who talks about the same things
- Kiran Gopinathan7 talks
- Işıl Dillig21 talks
- Nadia Polikarpova24 talks
- Shachar Itzhaky7 talks
- Michael Sammler16 talks
- Derek Dreyer35 talks
| title | conference | date |
|---|---|---|
| Answer Set Programming for Egg Extraction and More | EGRAPHS 2026 | 2026-06-15 |
Answer set programming encodes e-graphs as facts and finds low-cost extractions; a naive ASP encoding running with clingo and a core-guided (answer-core)… | ||
| Velvet: A Multi-Modal Verifier for Effectful Programs | Dafny 2026 | 2026-01-11 |
Velvet is a Dafny-style verifier implemented as a Lean library that verifies imperative programs with mutable state, loops, and nondeterminism by generating… | ||
| Lessons from Building an Auto-Active Verifier in Lean | Dafny 2026 | 2026-01-11 |
Veil is an auto‑active verifier implemented as a Lean library that does concrete and symbolic model checking, bounded searches, and inductive‑invariant… | ||
| Foundational Multi-Modal Program Verifiers | POPL 2026 | 2026-01-11 |
Paper presents a framework implemented in Lean implementation that provides a library of monad transformers for state, divergence, exceptions and… | ||
| Inductive Synthesis of Inductive Heap Predicates | OOPSLA 2025 | 2025-10-16 |
Claim: an algorithm synthesises recursive Separation Logic predicates from concrete heap graphs using positive-only ILP encoded in answer set programming… | ||
| Multi-Modal Verification of Distributed Systems in Lean | SAS 2025 | 2025-10-13 |
Framework called Veil (Lean library) encodes transition systems as shallow Lean programs, generates verification conditions sent to SMT solvers and falls back… | ||
| Opening | ICFP 2025 | 2025-10-12 |
Venue is Marina Bay Sands convention center with Orchid Plenary as the main room and lunches in Orchid Dining Hall; streaming runs from the Orchid West area… | ||
| Award Ceremony | ICFP 2025 | 2025-10-12 |
Selection process reports that 10 papers nominated are reviewed by a committee of six senior non‑conflicted members who meet twice and pick four distinguished… | ||
| General Chair Report | ICFP 2025 | 2025-10-12 |
About 600 on-site registrations, roughly half students, and about 30 collocated events; organizers report nearly 70 student volunteers, nine dedicated AV… | ||
| DSLs in Racket: You Want It How, Now? | SLE 2024 | 2024-10-20 |
Proposes a taxonomy of seven design intents and maps them to concrete Racket mechanisms, splitting enabling techniques into reader and expander customization… | ||
| Concurrent Data Structures Made Easy | OOPSLA 2024 | 2024-10-20 |
Library named OBatcher implements implicit batching in Multicore OCaml using async/await and functors; implicit-batching core is ~230 LOC, each generic… | ||
| Mechanised Hypersafety Proofs about Structured Data | PLDI 2024 | 2024-06-24 |
Claims a practical verification path: LGTM encodes formats as getter code and proves correctness via parametrised hypersafety triples mechanised as a Coq… | ||
| Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio... | CPP 2024 | 2024-01-15 |
Provides a library of definitions, lemmas and proof rules that let one switch between array and tree views (mutually derivable) to localize updates, formalizes… | ||
| Adventure of a Lifetime: Extract Method Refactoring for Rust | OOPSLA 2023 | 2023-10-23 |
An automated pipeline hoists a candidate function then applies staged repairs to satisfy Rust ownership and lifetimes, implemented as an IntelliJ Rust plugin… | ||
| Leveraging Rust Types for Program Synthesis | PLDI 2023 | 2023-06-17 |
First deductive synthesizer for safe Rust that uses Rust types to both shrink specifications and prune search, extracting programs from proofs and guaranteeing… | ||
| Mostly Automated Proof Repair for Verified Libraries | PLDI 2023 | 2023-06-17 |
Tool Sisyphus takes an old Coq-verified OCaml function, a changed OCaml implementation, and emits a mostly-automated Coq proof by combining dynamic program… | ||
| Certifying the Synthesis of Heap-Manipulating Programs | SPLASH 2022 | 2022-12-05 |
Method translates SuSLik synthesis traces into machine-checkable Coq proofs and produces three certifiers for HTT, Iris and VST, evaluated on 15 benchmarks… | ||
| Practical Smart Contract Sharding with Ownership and Commutativity Analysis | SPLASH 2022 | 2022-12-05 |
Static analysis tool CoSplit infers per-transition ownership and commutativity summaries for Cilla smart contracts and compiles them into sharding signatures… | ||
| Random Testing of a Higher-Order Blockchain Language (Experience Report) | ICFP 2022 | 2022-09-11 |
Integrates QuickChick on Coq with an OCaml implementation of a higher‑order smart‑contract language and builds a semantic harness by turning the monadic… | ||
| The Future of Concurrency and Parallelism | POPL 2022 Virtual Workshop | 2022-01-27 |
Panelists contrast concrete methods and hard surprises: mechanized proofs in Coq/Agda and concurrent separation logic are used to prove deadlock freedom and… | ||
| Automatically Synthesising Programs that We Can Trust | PLMW @ POPL 2022 | 2022-01-17 |
Claims an automated synthesiser called SuSLik generates imperative C-like programs plus machine checkable proofs and that those proofs are verifiable in Coq… | ||
| nothing matches | ||