CoqPL 2022
2022-01-22
-- online --
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
as the organisers put it
The CoqPL workshop series is an opportunity for programming languages researchers to meet and interact with one another and with members from the core Coq development team. We will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes, and work to strengthen the vibrant community around our favorite proof assistant. Topics in Scope Formalizations of PL research in Coq Experience reports from Coq users in research, education, and industry General-purpose libraries and tactic language extensions Domain-specifi ...
| title | author | length |
|---|---|---|
| Coq meets literate programming: tools for documenting, preserving, and sharing | Clément Pit-Claudel | 01h 02m |
Alectryon is a literate‑programming toolkit that records Coq output and embeds captured goals and messages into pre‑rendered HTML so proofs are instantly… | ||
| A Visual Ltac Debugger in CoqIDE | Jim Fehrle | 21m |
A visual Ltac debugger in CoqIDE (Coq 8.15) shows a concrete prototype: set a breakpoint on idtac, run and stop before the idtac, view call stack and local… | ||
| Scrap your boilerplate definitions in 10 lines of Ltac! | Qianchuan Ye, Benjamin Delaware | 20m |
Library IDT generates new inductive definitions from existing ones by running Template-Coq code driven by small Ltac constructor-transformer tactics, so dozens… | ||
| Tealeaves: Categorical structures for syntax | lawrence dunn, steve zidenzwick | 25m |
Tealeaves is a Coq library that provides a typeclass for syntax-like datatypes based on decorated-traversable monads and exposes a context-sensitive iterator… | ||
| Towards a Formalization of Nominal Sets in Coq | Fabricio Paranhos | 20m |
Formalization of nominal sets in Coq 8.14 implements list-of-swaps permutations and a type-class hierarchy for groups and actions, proving support, freshness… | ||
| A Case for Lightweight Interfaces in Coq | David Swasey, Paolo G. Giarrusso, Gregory Malecha | 17m |
Bedrock uses Coq and the Iris program logic to verify a large concurrent C++ hypervisor stack and finds Coq’s lack of lightweight interface files hurts scale… | ||
| Verifying Concurrent, Crash-Safe Systems with Perennial | jota sorority | 55m |
Perennial is a mechanized extension of Iris that proves crash safety for concurrent programs and imports Go via goose to verify real code; it verifies the… | ||
| A Verified Pipeline from a Specification Language to Optimized, Safe Rust | Rasmus Holdsbjerg-Larsen, Amin Timany | 17m |
A verified pipeline converts hacspec executable specs to optimized, safe Rust by adding a Coq backend for hacspec, synthesizing low-level code with Fiat… | ||
| Session with the Coq Development Team | Matthieu Sozeau, Yves Bertot, Emilio Gamba | 43m |
Coq 8.14 and 8.15 introduce a new case representation change that fixes surprising match-occurrence bugs and a Metacoq-checked subject reduction proof; native… | ||
| nothing matches | ||