CoqPL 2023
2023-01-21
Boston, United States
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
who it's for
Coq users and contributors, programming languages researchers, verified compiler engineers, formal methods researchers, security and privacy researchers, logic and mathematics educators, tool and IDE integrators
topics
demonic nondeterminism semantics; ZFC formalization in Coq; modular compiler verification; equivalence preserving compilation; graphical proof interface; coq-actema plugin integration; Path ORAM formalization; computational indistinguishability proofs; verified differential privacy mechanisms; monoidal categories for binders; MWP complexity analysis in Coq; Coq releases and Ltac2 development
| title | author | length |
|---|---|---|
| Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) | Samuel Gruetter | 56m |
Defines operational judgments that map a start state to a set of outcomes so one derivation captures every nondeterministic run, formalized in Coq and used… | ||
| Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set T... | Xinyi Wan, Qinxiang Cao | 34m |
A Coq deep embedding of ZFC and a textbook-style deduction system plus a small automation layer produce a mini ZFC prover that hides Coq internals and exposes… | ||
| Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati... | Dustin Jamner, Gabriel Kammer, Adam Chlipala | 31m |
A Coq framework for modular, extensible compiler verification that proves an inductive equivalence preservation theorem so adding one feature requires one new… | ||
| Integrating graphical proofs in Coq | Pablo Donato, Benjamin Werner, Kaustuv Chaudhuri | 26m |
A prototype called Actema implements gesture-driven proof construction and integrates with Coq via a coq-actema plugin using a client–server protocol: goals… | ||
| Towards Formally Verified Path ORAM in Coq | Hannah Leung, Talia Ringer, Christopher W. Fletcher | 28m |
Formalization of Path ORAM proceeds from a Python prototype to a Coq/Gallina formalization on GitHub, with the claim of machine-checked proofs of functional… | ||
| Verified Differential Privacy for Finite Computers | Vivien Rindisbacher, Arthur Azevedo de Amorim, Marco Gaboardi | 27m |
Coq formalization implements the Geometric Truncated Mechanism using Coq with finprob and rat and proves both an approximate bound (Alpha Prime) and when… | ||
| Formalizing Monoidal Categories and Actions for Syntax with Binders | Benedikt Ahrens, Ralph Matthes, Kobe Wullaert | 23m |
Mechanization of syntax with binders uses Coq + UniMath to formalize semantic signatures, initial algebras, monad-like substitution and the notion of strength… | ||
| Certifying Complexity Analysis | Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller | 29m |
Plans to formalize the MWP imperative analysis in Coq, with an IMP-like language, MathComp matrices and a type system, and to prove the key soundness theorem… | ||
| Session with the Coq Development Team | Yves Bertot, Maxime Dénès | 56m |
Two releases land in 2022 and Coq 8.16 ships on Sept 5 with the matching platform arriving Oct 10, and an 8.17 release candidate (fsrc1) is out with the… | ||
| nothing matches | ||