CoqPL 2020
2020-01-25
New Orleans, United States
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
| title | author | length |
|---|---|---|
| SMTCoq: Safe and Efficient Automation in Coq | Chantal Keller | 59m |
Presenter: Chantal Keller
Presented at CoqPL'20, colocated with POPL 2020. | ||
| Verifying Concurrent Go Code in Coq with Goose | Tej Chajed | 29m |
A pipeline imports a practical subset of Go into Coq: a 2.5k‑line Go translator produces GooseLang programs that plug into Iris’s weakest‑precondition… | ||
| An Equations Tutorial | Matthieu Sozeau | 27m |
Equations lets you write Coq functions by equations with rich pattern matching and recursion that elaborate to pure Gallina and generate a rewrite database of… | ||
| Deriving Instances with Dependent Types | Arthur Azevedo de Amorim | 25m |
Automates building typeclass instances for Coq inductives: the deriving library generates EQ, Choice, Countable/Fin-like and other instances without plugins… | ||
| Autosubst 2: Reasoning with de Bruijn Terms and Substitutions | Kathrin Stark | 56m |
Presenter: Kathrin Stark
Presented at CoqPL'20, part of POPL 2020. | ||
| Towards Formally Verified Just-In-Time Compilation | Aurèle Barrière | 29m |
A Coq-based JIT middle-end prototype implements an RTL-like IR with an assume instruction (from Suya) to encode speculative checks, plus passes for speculation… | ||
| A Coq Library of Undecidable Problems | Yannick Forster | 31m |
A Coq library formalizes a large graph of undecidability reductions and actually produces executable artifacts: it mechanizes PCP, Hilbert’s tenth, first-order… | ||
| Session with the Coq Development Team | 44m | |
Coq announces concrete engineering changes and breaking-but-fixable migration details: 8.10 adds a new prop equality behavior, compact primitive fixed-size… | ||
| nothing matches | ||