CPP 2018- Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Full Citation in the ACM Digital Library

SESSION: Invited Talks

POPLMark reloaded: mechanizing logical relations proofs (invited talk)

Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)

SESSION: Verifing Programs and Systems

Total Haskell is reasonable Coq

A formal proof in Coq of a control function for the inverted pendulum

Completeness and decidability of converse PDL in the constructive type theory of Coq

SESSION: Verified Applications

Mechanising and verifying the WebAssembly specification

Towards verifying ethereum smart contract bytecode in Isabelle/HOL

Mechanising blockchain consensus

Formal microeconomic foundations and the first welfare theorem

SESSION: Proof Methods and Libraries

Triangulating context lemmas

Adapting proof automation to adapt proofs

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

Formal proof of polynomial-time complexity with quasi-interpretations

SESSION: Trusted Verification Frameworks and Systems

A verified SAT solver with watched literals using imperative HOL

Œuf: minimizing the Coq extraction TCB

Proofs in conflict-driven theory combination

SESSION: Type Theory, Set Theory, and Formalized Mathematics

Finite sets in homotopy type theory

Generic derivation of induction for impredicative encodings in Cedille

Large model constructions for second-order ZF in dependent type theory

A constructive formalisation of Semi-algebraic sets and functions

SESSION: Formalizing Meta-Theory

HOπ in Coq

A Coq formalization of normalization by evaluation for Martin-Löf type theory

A two-level logic perspective on (simultaneous) substitutions

Binder aware recursion over well-scoped de Bruijn syntax