Adam Chlipala
where else to find them
what they talk about
all 7 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski4 editions2023–2026
- POPL2 editions2021–2022
- OOPSLA2 editions2022–2025
all 9 in the filters
on a stage with
all 46 in the filters
who talks about the same things
- Andres Erbsen5 talks
- Jonathan Ragan-Kelley12 talks
- Samuel Gruetter5 talks
- Clément Pit-Claudel17 talks
- Ranjit Jhala19 talks
- Benjamin Delaware18 talks
| title | conference | date |
|---|---|---|
| A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs | PLDI 2026 | 2026-06-15 |
Mechanized framework extends ATL and uses the Rock proof assistant to produce a verified compression/decompression adjoint that rewrites dense tensor kernels… | ||
| Causality and Semantic Separation | PLDI 2026 | 2026-06-15 |
Claim: a new semantic separation notion exactly matches graph-theoretic d-separation, with a full mechanized proof mechanized in Rocq. Construction uses… | ||
| Pyrosome: Verified Compilation for Modular Metatheory | OOPSLA 2025 | 2025-10-16 |
Pyrosome is a Coq framework that defines languages as lists of inference rules (GATs) and treats program equivalence as the reflexive‑transitive‑symmetric… | ||
| Research on Different Time Horizons (and an Example with Machine-Checked Proofs) | PLMW @ PLDI 2025 | 2025-06-16 |
Argues that long-horizon long-term systems work pays off by combining judgment with iterative prototyping, demonstrates end-to-end mechanized proofs using Coq… | ||
| Making Concurrent Hardware Verification Sequential | PLDI 2025 | 2025-06-16 |
Introduces Fjfj, a Bluespec-like language that removes exponential proof cases by separating action methods vs value methods and forbidding multiple action… | ||
| Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…) | PLDI 2025 | 2025-06-16 |
Formal definition of cryptographic constant‑time for languages with compiler‑resolved nondeterminism using omnisemantics and single‑copy assertions, mechanized… | ||
| 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… | ||
| A Verified Compiler for a Functional Tensor Language | PLDI 2024 | 2024-06-24 |
A mechanically verified implementation of a lowering algorithm for ATL proves that a functional tensor program lowers to imperative loop nests that write… | ||
| Live Verification in an Interactive Proof Assistant | PLDI 2024 | 2024-06-24 |
Prototype implements live verification after each line inside Coq, parsing polyglot C/Coq files and updating a concise symbolic state view while editing; it… | ||
| Foundational Integration Verification of a Cryptographic Server | PLDI 2024 | 2024-06-24 |
A verified bare-metal garage-door server implements authenticated open/close commands and prevents replays by rotating seeds, and a single machine-checked… | ||
| Flexible Instruction-Set Semantics via Abstract Monads | ICFP 2023 | 2023-09-04 |
Claims a single Haskell-based core semantics, parameterized by a Risk5Machine type class over monads, supports testing, interactive proof, model checking and… | ||
| Hardware Verification of Timing Side Channel Freedom in the Spectre Era | PLARCH 2023 | 2023-06-17 |
Claim: a synthesizable, pipelined two-core RISC-V design plus a hardware security monitor enforces strong timing isolation and is proven equivalent to an… | ||
| CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives | PLDI 2023 | 2023-06-17 |
CryptOpt turns Fiat Cryptography IR into x86-64 assembly by running a random local search over instruction selection and scheduling, auto-benchmarking… | ||
| Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati... | CoqPL 2023 | 2023-01-21 |
A Coq framework for modular, extensible compiler verification that proves an inductive equivalence preservation theorem so adding one feature requires one new… | ||
| Fast Cryptographic Code via Partial Evaluation | PEPM 2023 | 2023-01-16 |
Generates mechanically verified, high-performance cryptographic C from Coq: a verified compiler using partial evaluation, abstract interpretation and… | ||
| C4: verified transactional objects | OOPSLA 2022 | 2022-12-05 |
C4 claims a mechanized, compositional way to prove both linearizability and strict serializability and to stitch those proofs together for mixed… | ||
| Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites | POPL 2022 | 2022-01-16 |
A Coq-verified framework implements a pure functional tensor IR called ATL and a suite of semantics-preserving, source-to-source rewrites plus reshape… | ||
| Certifying Derivation of State Machines from Coroutines | POPL 2022 | 2022-01-16 |
A compiler implemented as a Coq tactic turns programs written with freer-monad coroutines into explicit state-machine code by searching for equivalence proofs… | ||
| Automated Synthesis of Verified Firewalls | CoqPL 2021 | 2021-01-19 |
A verified-compiler pipeline turns a high-level firewall DSL (iptables-like history queries and monadic composition) into executable OCaml using Fiat synthesis… | ||
| Automated Synthesis of Verified Firewalls | POPL 2021 | 2021-01-17 |
Claim of correct-by-construction, stateful TCP/IP packet filters implemented as a verified compiler in Coq using the Fiat refinement framework and the… | ||
| Strong Formal Verification For RISC V: From Instruction Set Manual To RTL | 7th RISC-V Workshop 2017 | 2017-11-28 |
Claims a full machine-checked refinement from the RISC‑V ISA to RTL using a Coq proof assistant guided framework and a Bluespec-like language that compiles to… | ||
| nothing matches | ||