CoqPL 2021
2021-01-19
-- online --
CoqPL ·
[CoqPL 2020, CoqPL 2021, CoqPL 2022, CoqPL 2023, CoqPL 2024, CoqPL 2025]
| title | author | length |
|---|---|---|
| Verifying a compiler through equational means | Yannick Zakowski | 01h 06m |
Library code models LLVM-like IR as coinductive Interaction Trees and a companion Vellvm semantics on GitHub, represents each syntax node as an ITree with… | ||
| Session with the Coq Development Team | Matthieu Sozeau, Enrico Tassi | 46m |
Coq 8.13 appears: compile libraries with 8.13 to see new hint warnings and migrate by changing a hint’s attribute from global to export so it only activates… | ||
| A Limited Case for Reification by Type Inference | Jason Gross | 14m |
Reification by type inference shows that Coq’s notation system plus type inference can build a structured representation of curried argument types without… | ||
| Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml | Xuanrui Qi, Jacques Garrigue | 15m |
Formalizes OCaml GADT behavior by building a Coq mechanization of a core ML with structural polymorphism, recursive types and type-level equality; finds a… | ||
| Automated Synthesis of Verified Firewalls | Shardul Chiplunkar, Clément Pit-Claudel, Adam Chlipala | 12m |
A verified-compiler pipeline turns a high-level firewall DSL (iptables-like history queries and monadic composition) into executable OCaml using Fiat synthesis… | ||
| Verification of Algorithm and Code Generation for Signal Transforms | Patrick Brinich, Jeremy Johnson | 14m |
A formalization verifies a nontrivial subset of SPIRAL: SPL rewrite rules are proven to preserve matrix semantics and a Coulee–Tukey factorization is proved by… | ||
| Record Updates in Coq | Tej Chajed | 10m |
Library coq-record-update implements record setters by generating per-field setters with Ltac and plugging that Ltac into type class resolution so Coq runs the… | ||
| An experience report on writing usable DSLs in Coq | Clément Pit-Claudel, Thomas Bourgeat | 10m |
A hardware DSL called koika is implemented as a deeply embedded AST in Coq with a few thousand lines of code and hundreds of lines of notations; usability… | ||
| nothing matches | ||