CoqPL 2025
2025-01-25
Denver, United States
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
who it's for
Coq contributors and users, programming languages researchers, formal verification engineers, tactic and plugin authors, compiler and language designers, systems and network verification engineers, quantum computing formalizers
topics
Elpi rule-based meta-language; higher-order abstract syntax; Ltac2 context cleaning; GPT-4 C synthesis; Verified Software Toolchain verification; interaction trees for LLVM; Coq to OCaml extraction; mining Coq proof patterns; formal stabilizer quantum codes; verified linear algebra (mathcomp); session types logical relation; differential operators change structures
| title | author | length |
|---|---|---|
| Elpi: rule-based meta-languge for Rocq | Enrico Tassi | 51m |
Elpi is a rule-based meta-language that implements new Rocq commands and tactics by manipulating open terms with binders and holes, using higher-order abstract… | ||
| Towards Automated Verification of LLM-Synthesized C Programs | Prasita Mukherjee, Benjamin Delaware | 22m |
SYNVER is a pipeline that uses GPT-4 to synthesize C programs and a Verified Software Toolchain backend with an Ltac layer called SEauto to discharge proofs… | ||
| Vellvm: Formalizing the Informal | Calvin Beck, Hanxi Chen, Steve Zdancewic | 23m |
Formal Coq semantics for a large subset of LLVM IR uses interaction trees (coinductive freemonads) plus event handlers to capture nondeterminism and a… | ||
| Towards Mining Robust Coq Proof Patterns | Cezary Kaliszyk, Xuan-Bach D. Le, Christine Rizkallah | 19m |
Plans to mine a published Coq dataset for historical breakage and repair patterns, convert Coq scripts into lightweight ASTs, apply tree differencing to… | ||
| Implementing OCaml APIs in Coq | Joshua M. Cohen | 19m |
Extraction is modified to map Coq encodings of OCaml effects to real OCaml exceptions and refs so extracted code matches existing APIs while remaining… | ||
| Formal Verification of Quantum Stabilizer Code | Qiuyi Feng, Udaya Parampalli, Christine Rizkallah | 19m |
Formalization in Coq of the stabilizer-group algebra and an n‑qubit Pauli/phase construction yields proved algebraic properties (eigenvalues, generators) and a… | ||
| Towards Verified Linear Algebra Programs Through Equivalence | Yihan Yang, Mohit Tekriwal, John Sarracino, Matthew Sottile, Ignacio Laguna | 22m |
Extends the Coq mathcomp libraries with dot product, projection and basis theorems and uses them to mechanize Classical Gram‑Schmidt, proving nonzero outputs… | ||
| A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types | Tarakaram Gollamudi, Jules Jacobs, Yue Yao, Stephanie Balzer | 21m |
Proves termination for intuitionistic linear logic session types (ILLST) by building a semantic unary logical relation and showing the fundamental theorem… | ||
| Towards general white-box automation: a typeclass-guided context cleaner | Thibaut Pérami | 22m |
Built a small Ltac2 clarifier called cdestruct that uses typeclass-guided hints to run only safe, non‑backtracking context cleanup: case splits… | ||
| Formal Verification of a Software Defined Delay-Tolerant Network | Jan-Paul Ramos-Davila | 25m |
Claims a verified path from a P4 match‑action pipeline to network‑calculus guarantees by building NetQIR, a domain‑specific IR, a compiler from a restricted P4… | ||
| A Framework of Differential Operators | Runqing Xu, Sebastian Erdweg | 23m |
A Coq formalization presents a reusable framework that defines change structures (value, delta, patch, valid-change relation) and proves correctness of… | ||
| nothing matches | ||