Nada Amin
where else to find them
what they talk about
all 10 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2026
- PEPM2 editions2025–2026
- POPL2 editions2022–2026
all 18 in the filters
on a stage with
all 46 in the filters
who talks about the same things
- Yizhou Zhang13 talks
- Steve Zdancewic19 talks
- Tiark Rompf24 talks
- Nadia Polikarpova24 talks
- Amal Ahmed25 talks
- Işıl Dillig21 talks
| title | conference | date |
|---|---|---|
| Compiling to Recurrent Neurons | PLDI 2026 | 2026-06-15 |
Defines a linearly typed higher-order language Cajal(N) that compiles iteration and conditionals into matrices realized as recurrent neurons, proves a compiler… | ||
| Holey: Staged Execution from Python to SMT (Talk Proposal) | PEPM 2026 | 2026-01-11 |
Holey is a Python library that stages satisfiability predicates to SMT by dynamic operator overloading and light AST rewriting, emits portable SMT‑LIB, swaps… | ||
| Compiling to Linear Neurons | POPL 2026 | 2026-01-11 |
Claims a typed linear language called Cajal compiles discrete programs into linear neurons by translating conditionals into soft branching linear maps, with a… | ||
| Beyond Cons: Purely Relational Data Structures | miniKanren and Relational Programming Workshop 2025 | 2025-10-17 |
Adds a constraint-enabled extension to miniKanren that implements first-class set objects and association-list constraints, giving membership, set… | ||
| The Modular Imperative: Rethinking LLMs for Maintainable Software | LMPL 2025 | 2025-10-12 |
Runs experiments with cursor and cloud sonnet 4 and finds models default to monolithic code, often amplifying complexity and introducing bugs when porting or… | ||
| Multi-stage Relational Programming | PLDI 2025 | 2025-06-16 |
Implements a multi-stage extension of miniKanren that compiles known parts of relational interpreters and defers unknown holes to a runtime relational… | ||
| Collapsing Towers for Side-Channel Security | PEPM 2025 | 2025-01-21 |
A technique uses staging to turn an instrumented interpreter into a compilerlike residue program that exposes a runtime step counter and cache effects as… | ||
| dafny-annotator: AI-Assisted Verification of Dafny Programs | Dafny 2025 | 2025-01-19 |
Built a tool called dafny-annotator that uses LLMs plus greedy search (five iterations, five candidates) to insert invariants, decreases, and assertions into… | ||
| VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…) | Dafny 2025 | 2025-01-19 |
VerMCTS combines a logical verifier, an LLM (FinCode Llama v2), and a modified Monte Carlo Tree Search to synthesize Dafny and Coq programs and proofs; it… | ||
| Semantics of the memo Probabilistic Programming Language | LAFI 2025 | 2025-01-19 |
Formal semantics for the memo probabilistic programming language claim: a frame of mind is the core state that records choices, subframes and equations and… | ||
| DafnyBench: A Benchmark for Formal Software Verification | Dafny 2025 | 2025-01-19 |
DafnyBench is a scraped benchmark of 750 programs and ~53,000 LOC that tests whether LLMs (GPT‑4, Claude 3, etc.) can auto-generate the missing Dafny… | ||
| Persimmon: Nested Family Polymorphism with Extensible Variant Types | OOPSLA 2024 | 2024-10-20 |
Persimmon implements nested family polymorphism with extensible variant types, using a linkage concatenation representation to combine inherited and new… | ||
| Oxidize: A Step-Debugger for Static Semantics | IWACO 2023 | 2023-10-24 |
A static step-debugger for Rust-like ownership semantics that actually simulates the borrow checker by stepping three explicit contexts: a type context, a… | ||
| Exploratory Study on Multi-User Program Synthesis: A Multi-Wizard Approach | HATRA 2023 | 2023-10-22 |
Proposes two study designs: a between-subjects lab with 24 participants (pairs vs individuals, each doing one task with and one without a synthesizer) and a… | ||
| LURK: Lambda, the Ultimate Recursive Knowledge | ICFP 2023 | 2023-09-04 |
Lurk is a LISP-based language plus a universal interpreter circuit that lets programs be supplied as data so zk proofs verify runs instead of flattened… | ||
| Extensible Metatheory Mechanization via Family Polymorphism | PLDI 2023 | 2023-06-17 |
Claims a language-layer for family polymorphism inside Coq that reuses code and proofs via late binding and generates a Coq plugin plus a core dependent type… | ||
| Reasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence | POPL 2022 | 2022-01-16 |
Formal semantics for a core PPL with continuous distributions, scoring, nested queries and general recursion defines mutually recursive semantics so… | ||
| Adventures in extending miniKanren | miniKanren 2021 | 2021-08-26 |
Adds a stage miniKanren interpreter that turns interpreters into compilers and an SMT-backed CLP SMT extension by augmenting the miniKanren state with extra… | ||
| Full Workshop | miniKanren 2021 | 2021-08-26 |
Symbolic execution produces a symbolic scheme that exposes schedule, unification and reification costs and shows scheduling dominates some pathologies… | ||
| Functional Programming for COVID 19 Drug Repurposing | PLMW @ ICFP 2020 | 2020-08-23 |
A reasoning engine called mediKanren implemented in Racket and miniKanren mines merged biomedical knowledge graphs (40 sources, SemMedDB ~97M edges) to propose… | ||
| Collapsing Towers of Interpreters | Code Mesh 2017 | 2017-11-08 |
Claims that an interpretive tower can be reduced to a one-pass compiler are demonstrated by a staged, stage-polymorphic calculus plus two prototypes: a dynamic… | ||
| DOT: Scala Types from Theory to Practice | Scala World 2017 | 2017-09-16 |
Presents Dependent Object Types as the core calculus used in Dotty, proves soundness by modeling path‑dependent type members, unions/intersections and a store… | ||
| Generative Programming and Verification | EuroClojure 2017 | 2017-07-20 |
A <500-line SQL engine is implemented in Scala that starts as a relational-algebra interpreter and, via lightweight modular staging and Scala’s type system… | ||
| Programming Should Eat Itself | Strange Loop 2014 | 2014-09-17 |
Argues that interpreters can be stacked and mutated so programs describe and change their own semantics, and demos a reflective language called Black… | ||
| From Greek to Clojure! | Clojure/conj 2013 | 2013-11-14 |
Translates paper inference rules into working Clojure: implements Peano naturals and a three‑place plus as both a function and a relation, a simply‑typed… | ||
| nothing matches | ||