Nadia Polikarpova
where else to find them
x:polikarn
linkedin:nadia-polikarpova
what they talk about
all 11 in the filters
where they keep going back
- OOPSLA4 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2022–2024
- POPL2 editions2023–2026
all 11 in the filters
on a stage with
all 53 in the filters
who talks about the same things
- Armando Solar-Lezama18 talks
- Işıl Dillig21 talks
- Steve Zdancewic19 talks
- Loris D'Antoni17 talks
- Deepak Garg18 talks
- Shachar Itzhaky7 talks
| title | conference | date |
|---|---|---|
| ChopChop: A Programmable Framework for Semantically Constraining the Output of Language(…) | POPL 2026 | 2026-01-11 |
ChopChop constructs constrained decoders that decide whether a token prefix has a completion satisfying a semantic spec by building prefix spaces and solving a… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | OOPSLA 2025 | 2025-10-16 |
Laurel is a tool that generates missing Dafny assertions with LLMs by (1) inserting an assertion placeholder at the SMT error location and (2) supplying… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | Dafny 2025 | 2025-01-19 |
Laurel uses large language models to auto-generate missing Dafny assertions and reports a >56.6% success rate on a new DafnyGym benchmark of lemmas extracted… | ||
| AI-Assisted Programming Today and Tomorrow | PLDI 2024 | 2024-06-24 |
Recent studies find GitHub Copilot has over 1M paid users and generates roughly 30–40% of active users’ code; a grounded study of 20 programmers identifies two… | ||
| Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis | PLDI 2024 | 2024-06-24 |
Superfusion uses inductive program synthesis to remove intermediate collections by synthesizing a small compression function that maps packed structures to… | ||
| Grounded Copilot: How Programmers Interact with Code-Generating Models | OOPSLA 2023 | 2023-10-23 |
Study watches 20 programmers across four tasks and languages and builds a grounded-theory claim that interactions with Copilot are bimodal: acceleration mode… | ||
| 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… | ||
| Big Ideas in Program Synthesis | PLMW @ POPL 2023 | 2023-01-17 |
Survey of program synthesis highlights three concrete tactics and working tools: observational equivalence prunes enumerative search by keeping one… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| babble: Learning Better Abstractions with E-Graphs and Anti-unification | POPL 2023 | 2023-01-15 |
Presents Library Learning Modulo Theory (LLMT) implemented as the tool babble, which uses e-graphs plus a new e-graph anti-unification algorithm and targeted… | ||
| 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… | ||
| Welcome | Haskell Symposium 2022 | 2022-09-15 |
Short welcome and program highlights: an immediate keynote on ultrabike effects (GitHub) and tomorrow a keynote from the Haskell Foundation about what’s next… | ||
| PC Chair Report | Haskell Symposium 2022 | 2022-09-15 |
Program committee experiments remove the no early round option and introduce a separate abstract deadline to start reviews sooner. Submissions: 22 abstracts… | ||
| Searching Entangled Program Spaces | ICFP 2022 | 2022-09-11 |
Introduces equality-constrained tree automata to compactly represent program spaces where subterm choices are entangled, and implements extraction and lazy… | ||
| Type-Directed Program Synthesis for RESTful APIs | PLDI 2022 | 2022-06-13 |
Built a tool called epiphany that infers fine-grained semantic types from OpenAPI docs plus thousands of observed API call traces, uses a type-directed… | ||
| LooPy: Interactive Program Synthesis with Control Structures | OOPSLA 2021 | 2021-10-17 |
A Live Programming–integrated synthesizer called LooPy extends Small-Step Live PBE to handle loops by treating holes as runtime pauses and asking the… | ||
| STORM: Refinement Types for Secure Web Applications | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
Storm is a web framework that enforces data-dependent security policies at compile time via a Security Typed ORM that refines MVC types with logical… | ||
| Just-in-Time Learning for Bottom-Up Enumerative Synthesis | OOPSLA 2020 | 2020-11-15 |
Builds a solver called Probe that uses just-in-time learning to update PCFG production costs from cheapest partial solutions and then runs guided bottom-up… | ||
| Digging for Fold: Synthesis-Aided API Discovery for Haskell | OOPSLA 2020 | 2020-11-15 |
A synthesis-backed search called Hoogle Plus indexes popular Haskell libraries and synthesizes compositions that match either a provided type or inferred types… | ||
| Constraint Solvers for the Working PL Researcher | PLMW @ ICFP 2020 | 2020-08-23 |
Demonstrates using Z3 Python bindings to build a small toolchain that does constraint-based declarative execution, verification, and synthesis. Encodes array… | ||
| Liquid Information Flow Control | ICFP 2020 | 2020-08-23 |
Claims a new DSL called Lifty domain-specific language that encodes information-flow policies as liquid refinements and enforces them with a TIO-style security… | ||
| Liquid Resource Types | ICFP 2020 | 2020-08-23 |
Liquid Resource Types claims an automated refinement-type system that proves precise, value-dependent resource bounds (polynomial, exponential and fine-grained… | ||
| Type-Driven Program Synthesis | Strange Loop 2018 | 2018-09-26 |
Claims an automatic, SMT-backed refinement type checker that turns specifications into code and produces machine-checked guarantees. Synquid synthesizes… | ||
| nothing matches | ||