CPP 2020
29 papers
- A constructive formalization of the weak perfect graph theorem
- A formal proof of the independence of the continuum hypothesis
- A functional proof pearl: inverting the Ackermann hierarchy
- A mechanized formalization of GraphQL
- A verified packrat parser interpreter for parsing expression grammars
- An equational theory for weak bisimulation via generalized parameterized coinduction
- Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq
- ConCert: a smart contract certification framework in Coq
- Coq à la carte: a practical approach to modular syntax with binders
- Cubical synthetic homotopy theory
- Exploration of neural machine translation in autoformalization of mathematics in Mizar
- Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL
- Formalising perfectoid spaces
- Formalizing determinacy of concurrent revisions
- Formalizing π-calculus in guarded cubical Agda
- FreeSpec: specifying, verifying, and executing impure computations in Coq
- Frying the egg, roasting the chicken: unit deletions in DRAT proofs
- Intrinsically-typed definitional interpreters for linear, session-typed languages
- Matching logic: the foundation of the K framework (invited talk)
- Proof assistants at the hardware-software interface (invited talk)
- Proof pearl: Braun trees
- REPLica: REPL instrumentation for Coq analysis
- The Poincaré-Bendixson theorem in Isabelle/HOL
- The lean mathematical library
- Three equivalent ordinal notation systems in cubical Agda
- Undecidability of higher-order unification formalised in Coq
- Verified programming of Turing machines in Coq
- Verified security of BLT signature scheme
- Verifying x86 instruction implementations