CPP 2021
26 papers
- A Coq formalization of data provenance
- A formal proof of PAC learnability for decision stumps
- A minimalistic verified bootstrapped compiler (proof pearl)
- A modular Isabelle framework for verifying saturation provers
- A novice-friendly induction tactic for lean
- A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems
- An Isabelle/HOL formalization of AProVE's termination method for LLVM IR
- An anti-locally-nameless approach to formalizing quantifiers
- CertRL: formalizing convergence proofs for value and policy iteration in Coq
- Contextual refinement of the Michael-Scott queue (proof pearl)
- Developing and certifying Datalog optimizations in coq/mathcomp
- Extracting smart contracts tested and verified in Coq
- Formal verification of authenticated, append-only skip lists in Agda
- Formal verification of semi-algebraic sets and real analytic functions
- Formalizing category theory in Agda
- Formalizing the ring of Witt vectors
- Lassie: HOL4 tactics by example
- Lutsig: a verified Verilog compiler for verified circuit development
- Machine-checked semantic session typing
- On the formalisation of Kolmogorov complexity
- Reasoning about monotonicity in separation logic
- Teaching algorithms and data structures with a proof assistant (invited talk)
- The generalised continuum hypothesis implies the axiom of choice in Coq
- Towards efficient and verified virtual machines for dynamic languages
- Towards formally verified compilation of tag-based policy enforcement
- Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk)