- Joshua Clune:
A Formalized Reduction of Keller's Conjecture. CPP 2023: 90-101 - Matthew L. Daggitt
, Robert Atkey
, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi
:
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. CPP 2023: 102-120 - Floris van Doorn, Patrick Massot, Oliver Nash
:
Formalising the h-Principle and Sphere Eversion. CPP 2023: 121-134 - Michael Färber
:
Terms for Efficient Proof Checking and Parsing. CPP 2023: 135-147 - Hugo Férée, Sam van Gool:
Formalizing and Computing Propositional Quantifiers. CPP 2023: 148-158 - Benjamin Grégoire, Jean-Christophe Léchenet
, Enrico Tassi:
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP 2023: 167-181 - Yann Herklotz
, Delphine Demange, Sandrine Blazy:
Mechanised Semantics for Gated Static Single Assignment. CPP 2023: 182-196 - Cezary Kaliszyk:
Improved Assistance for Interactive Proof (Keynote). CPP 2023: 2 - Christina Kohl
, Aart Middeldorp:
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. CPP 2023: 197-210 - Katherine Kosaian
, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. CPP 2023: 211-224 - Angeliki Koutsoukou-Argyraki
, Mantas Baksys, Chelsea Edmonds
:
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. CPP 2023: 225-238 - Thomas Lamiaux
, Axel Ljungström, Anders Mörtberg:
Computing Cohomology Rings in Cubical Agda. CPP 2023: 239-252 - Jannis Limperg
, Asta Halkjær From
:
Aesop: White-Box Best-First Proof Search for Lean. CPP 2023: 253-266 - Bhavik Mehta:
Formalising Sharkovsky's Theorem (Proof Pearl). CPP 2023: 267-274 - Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy:
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. CPP 2023: 275-289 - Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
:
Formalising Decentralised Exchanges in Coq. CPP 2023: 290-302 - Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster:
P4Cub: A Little Language for Big Routers. CPP 2023: 303-319 - Brae J. Webb
, Ian J. Hayes, Mark Utting:
Verifying Term Graph Optimizations using Isabelle/HOL. CPP 2023: 320-333 - Kexing Ying, Rémy Degenne:
A Formalization of Doob's Martingale Convergence Theorems in mathlib. CPP 2023: 334-347 - Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 [contents] - 2022
- Benedikt Ahrens
, Ralph Matthes
, Anders Mörtberg
:
Implementing a category-theoretic framework for typed abstract syntax. CPP 2022: 307-323 - Guillaume Ambal, Sergueï Lenglet, Alan Schmitt:
Certified abstract machines for skeletal semantics. CPP 2022: 55-67 - June Andronick:
The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). CPP 2022: 1 - Andrew W. Appel
:
Coq's vibrant ecosystem for verification engineering (invited talk). CPP 2022: 2-11 - Jeremy Avigad
, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman:
A verified algebraic representation of cairo program execution. CPP 2022: 153-165 - Quentin Carbonneaux, Noam Zilberstein
, Christoph Klee, Peter W. O'Hearn
, Francesco Zappa Nardelli:
Applying formal verification to microkernel IPC at meta. CPP 2022: 116-129 - Hing-Lun Chan
:
Windmills of the minds: an algorithm for fermat's two squares theorem. CPP 2022: 251-264 - Louis Cheung
, Liam O'Connor
, Christine Rizkallah
:
Overcoming restraint: composing verification of foreign functions with cogent. CPP 2022: 13-26 - Esther Conrad
, Laura Titolo
, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle
:
A compositional proof framework for FRETish requirements. CPP 2022: 68-81 - Pablo Donato
, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. CPP 2022: 197-209