Clément Pit-Claudel
where else to find them
what they talk about
all 7 in the filters
where they keep going back
all 10 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Aurèle Barrière7 talks
- Adam Chlipala23 talks
- Thomas Bourgeat9 talks
- Michael Sammler16 talks
- Peter Sewell14 talks
- Rastislav Bodík8 talks
| title | conference | date |
|---|---|---|
| Scalable Type Inference for Intrinsically-Typed Binders | RocqPL 2026 | 2026-01-17 |
Claims that guided type inference using bi-directionality hints plus automation in Ltac2 makes intrinsically-typed binders practical in Rocq: variable contexts… | ||
| Precise Reasoning about Container-Internal Pointers with Logical Pinning | CPP 2026 | 2026-01-12 |
Claims a lightweight borrowing discipline called logical pinning that decouples address exposure from ownership so container-internal pointers can be tracked… | ||
| Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics(…) | POPL 2026 | 2026-01-11 |
Paper presents a mechanized, ECMAScript‑faithful semantics for JavaScript regexes in the Rocq proof assistant, equating a concise 21 inductive rules semantics… | ||
| Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types | OOPSLA 2024 | 2024-10-20 |
Proposal implements a Scala extension called Gradient that lets legacy code be migrated incrementally to an object-capability model by combining runtime… | ||
| Linear Matching of JavaScript Regular Expressions | PLDI 2024 | 2024-06-24 |
Presents a proof that a much larger subset of JavaScript regexes admits linear-time matching, identifies semantic bugs and superlinear cases in V8’s linear… | ||
| 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… | ||
| Incremental Proof Development in Dafny with Module-Based Induction | Dafny 2024 | 2024-01-14 |
Claim: encoding Coq-style induction principles as module-based induction in Dafny makes iterative proofs stable and debuggable. Implementation: a list… | ||
| Diagrammatic notations for interactive theorem proving | HATRA 2023 | 2023-10-22 |
Argues that interactive theorem provers need declarative diagram languages that match text macros by delivering low-cost composition and good-looking idioms… | ||
| 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… | ||
| Coq meets literate programming: tools for documenting, preserving, and sharing | CoqPL 2022 | 2022-01-22 |
Alectryon is a literate‑programming toolkit that records Coq output and embeds captured goals and messages into pre‑rendered HTML so proofs are instantly… | ||
| 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… | ||
| An experience report on writing usable DSLs in Coq | CoqPL 2021 | 2021-01-19 |
A hardware DSL called koika is implemented as a deeply embedded AST in Coq with a few thousand lines of code and hundreds of lines of notations; usability… | ||
| 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… | ||
| An experience report on writing usable DSLs in Coq | POPL 2021 | 2021-01-17 |
A report on building a hardware DSL in Coq: the codebase totals a few thousand lines of Coq and hundreds of lines of notations; Coq 8.9 custom entries let the… | ||
| Untangling Mechanized Proofs | SLE 2020 | 2020-11-16 |
Alectryon is a Python toolkit that runs Coq on source files, captures tactic outputs and goals, and emits interactive web visualizations that inline inputs and… | ||
| nothing matches | ||