CoqPL 2024
2024-01-20
London, United Kingdom
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
who it's for
core Coq developers, proof assistant researchers, plugin and tool developers, formal methods engineers, compiler developers, programming language researchers, smart contract verification engineers
topics
formal OCaml FFI semantics; verified OCaml-C interoperability; Coq to WebAssembly compilation; WasmCert formalisation reuse; well-founded recursion with Acc proofs; functorial syntax via indexing categories; Hax to ConCert smart contract pipeline; formal blockchain voting proofs; MetaCoq inductive types typesetting; VSCoq standalone language server; coq-lsp dependency handling with effects; diagram editor for categorical proofs
| title | author | length |
|---|---|---|
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (I... | Armaël Guéneau | 01h 02m |
Melocoton gives a verified way to link OCaml and C: it supplies the first formal semantics of the OCaml FFI and a program logic that reasons end-to-end about… | ||
| CertiCoq-Wasm: Verified compilation from Coq to WebAssembly | Wolfgang Meier, Jean Pichon-Pharabod, Bas Spitters | 25m |
A verified compiler from Gallina (Coq) to WebAssembly is implemented and mechanised against the WasmCert-Coq formalisation, reusing the CertiCoq pipeline and… | ||
| Session with the Coq Development Team | Matthieu Sozeau, Yves Bertot, Emilio Jesús Gallego Arias | 01h 25m |
Coq releases 8.17–8.19 add concrete features: ability to disable notations locally and use temporary scopes with an underscore, Ltac2 gains arrays, maps and… | ||
| Well-founded recursion done right | Xavier Leroy | 21m |
Defines non-structural recursion by adding an extra accessibility proof argument and making recursion structural on that proof, so a function like gcd recurses… | ||
| Functorial Syntax for All | Piotr Polesiuk, Filip Sieczkowski | 21m |
A Coq library implements a variant of Fiore–Plotkin–Turi functorial syntax: users define syntax as functors over indexing categories and supply functorial and… | ||
| Specifying Smart Contract with Hax and ConCert | Lasse Letager Hansen, Bas Spitters | 16m |
A reproducible toolchain embeds Rust-style smart contracts into Hax, rewrites mutable state into message-passing state, annotates properties, and translates… | ||
| A formal security analysis of Blockchain voting | Nikolaj Sidorenco, Laura Brædder, Lasse Letager Hansen, Eske Hoy Nielsen, Bas Spitters | 26m |
Formal Coq development models the Open Vote Network and proves provably functionally correct behavior plus cryptographically secure properties: self‑tallying… | ||
| InducTeX: A MetaCoq plugin for typesetting inductive definitions | Jacco Krijnen | 22m |
Builds a MetaCoq plugin that quotes Coq inductives, inspects constructors in the TemplateMonad and pretty prints them as TeX inference rules, so it prints… | ||
| VsCoq 2, new foundations | Romain Tetley | 22m |
Full reimplementation of the VSCoq extension ships a standalone OCaml language server and a TypeScript React client with a reactive document model, a query… | ||
| Integrating Dependency Building with Document Checking in Coq | Emilio Jesús Gallego Arias, Bhakti Shah | 21m |
Prototype integrates a build system into coq-lsp by handling Require as an effect using algebraic effects in OCaml 5, so the server checks dependencies on… | ||
| A diagram editor to mechanize categorical proofs | Ambroise Lafont | 22m |
A diagram editor runs as a web app or Electron desktop app and hooks into Coq via VS Code + coq-lsp integration, showing diagrammatic goals as graphics and… | ||
| nothing matches | ||