CPP 2020
| title | author | length |
|---|---|---|
| Matching Logic: Foundation of the K Framework | Grigore Rosu | 01h 03m |
One formal semantics drives interpreters, verifiers and model checkers: a 5,000‑rule C11 semantics with a >120‑cell configuration compiles to LLVM and yields a… | ||
| A Verified Packrat Parser Interpreter for Parsing Expression Grammars | Clément Blaudeau | 23m |
A mechanically verified packrat parser interpreter for PEGs implements a small-step semantics and a static termination analysis (computing the… | ||
| Proof Pearl: Braun Trees | Tobias Nipkow | 21m |
Paper supplies verified code and machine-checked proofs that pin down concrete claims: computing size in log^2 time, building an all-equal tree with n nodes in… | ||
| FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq | Thomas Letan | 24m |
FreeSpec implements impure computations in Coq using a free monad over explicit interfaces and certifies them with contract types built from a computable… | ||
| Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs | Adrian Rebola Pardo | 20m |
Finds that many DRAT proofs rely on spurious unit deletions: CDCL solvers (e.g. MiniSat-style solver-remove-satisfied) emit deletions that keep propagated… | ||
| Weak Bisimulation via Generalized Parameterized Coinduction | Yannick Zakowski | 20m |
Claims a gPaco generalization of the Paco coinduction library that adds a second parameter to fix an information‑leak in parameterized coinduction, implemented… | ||
| REPLica: REPL Instrumentation for Coq Analysis | Talia Ringer | 24m |
REPLica instruments the Coq read‑eval‑print loop with a client‑server plugin and records every interaction (timestamps, REPL inputs and responses) across UIs… | ||
| Verified Programming of Turing Machines in Coq | Fabian Kunze | 22m |
Mechanized development of Turing machines and a verified programming framework in Coq that includes a library of machine encodings, a small verified… | ||
| A Functional Proof Pearl: Inverting the Ackermann Heirarchy | Linh Tran | 22m |
Claim: a certified algorithm computes the inverse Ackermann function for all n without constructing huge Ackermann values, formalized in Coq as a compact… | ||
| Undecidability of Higher-Order Unification Formalised in Coq | Simon Spies | 21m |
Mechanisation in Coq proves that second-order unification is undecidable and, via a conservative embedding, that all higher-order unification problems are… | ||
| Cubical Synthetic Homotopy Theory | Loïc Pujet | 25m |
Claims that computational univalence holds and higher inductive types give genuine computation are backed by a Cubical Agda development that redoes standard… | ||
| Three Equivalent Ordinal Notation Systems in Cubical Agda | Fredrick Nordvall Forsberg | 19m |
Three concrete ordinal notations for ordinals below ε0 are implemented in Cubical Agda: a subset-of-binary-trees giving canonical Cantor normal forms, a mutual… | ||
| CPP 2020 PC Chairs' Report | Cătălin Hriţcu | 31m |
Conference receives 72 submissions and accepts 27 papers (37.5%); review uses HotCRP and light double‑blind, with 26 PC members plus 79 external reviewers… | ||
| Proof Assistants At the Hardware-Software Interface | Adam Chipala | 56m |
A working FPGA testbed implements a verified Internet of Things light bulb with an Ethernet card, a processor and software stack written in calk and proved… | ||
| Coq a la Carte: A Practical Approach to Modular Syntax With Binders | Kathrin Stark | 20m |
Presents a Coq workflow that achieves practical modular syntax by using direct injections of variant copies instead of functor fixed points, plus generated… | ||
| GraphCoQL: A mechanized formalization of GraphQL in Coq | Tomas Diaz | 19m |
Mechanized formalization of GraphQL in Coq that defines a graph data model, implements a normalization algorithm and proves it correct and semantics-preserving… | ||
| ConCert: A Smart Contract Certification Framework in Coq | Danil Annenkov | 24m |
Framework converts ACORN smart contracts into Coq functions via MetaCoq, proves computational soundness of the translation, and embeds the resulting functions… | ||
| Formalising Oblivious Transfer in CryptHOL | David Butler | 22m |
Formalisation proves semi-honest security of a classic oblivious transfer construction inside Isabelle/HOL using the CryptHOL/Crypto probabilistic-programming… | ||
| Verified Security of BLT Signature Scheme | Ahto Truu | 24m |
Formalizes and mechanically verifies that a BLT-style signature scheme becomes existentially unforgeable when a forward‑resistant tagging primitive combines… | ||
| Formalizing Determinacy of Concurrent Revisions | Roy Overbeek | 17m |
Formalizes part of the 2011 concurrent revisions semantics in Isabelle formalization, proving determinacy (confluence modulo equivalence) by completing case… | ||
| Formalizing pi-Calculus in Guarded Cubical Agda | Niccolò Veltri | 25m |
Implements guarded extensions of Cubical Agda and formalizes an internal denotational model of the early pi-calculus; builds a higher-inductive finite powerset… | ||
| Intriniscly-Typed Interpretation of Linear Languages | Arjen Rouvoet | 16m |
Defines an intrinsically-typed definitional interpreter for session-typed languages with linear channels, implemented in Agda so semantics are executable and… | ||
| A Constructive Formalization of the Weak Perfect Graph Theorem | Abhishek Kr Singh | 22m |
Presenter: Abhishek Kr Singh
Presented at CPP'20, colocated with POPL 2020. | ||
| Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq | Christian Doczkal | 18m |
Formal proof in Coq (MathComp) shows completeness: an 11‑axiom equational theory proves two terms equivalent iff their interpreted directed labeled graphs are… | ||
| The Poincare-Bendixson Theorem in Isabelle/HOL | Yong Kiam Tan | 20m |
Formalizes the planar Poincare–Bendixson claim in Isabelle/HOL, building on the existing Jordan curve theorem and ODE/real-analysis libraries. Key result is a… | ||
| A formal proof of the independence of the continuum hypothesis | Jesse Han | 23m |
A complete formal proof that the Continuum Hypothesis is independent of ZFC is carried out in Lean 3: 20,000 lines and about a year of work produce a modular… | ||
| The Lean Mathematical Library | Robert Y. Lewis | 22m |
A community-driven library for Lean 3 assembles a large body of formalized mathematics plus automation: 74 contributors and a maintainer team that grows to 13… | ||
| Formalising Perfectoid Spaces | Johan M. Commelin | 25m |
Formalisation of perfectoid spaces in Lean produces a dependency graph where the central definition sits atop reused mathlib plus new code for valuation… | ||
| nothing matches | ||