CPP 2017- Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

Full Citation in the ACM Digital Library

SESSION: Keynotes

Porting the HOL light analysis library: some lessons (invited talk)

Mechanized verification of preemptive OS kernels (invited talk)

SESSION: Algorithm and Library Verification

Verifying a hash table and its iterators in higher-order separation logic

A formalization of the Berlekamp-Zassenhaus factorization algorithm

Formal foundations of 3D geometry to model robot manipulators

SESSION: Automated Proof and Its Formal Verification

BliStrTune: hierarchical invention of theorem proving strategies

Automatic cyclic termination proofs for recursive procedures in separation logic

Formalization of Karp-Miller tree construction on petri nets

SESSION: Formalized Mathematics with Numerical Computations

A Coq formal proof of the Lax-Milgram theorem

A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations

Markov processes in Isabelle/HOL

Formalising real numbers in homotopy type theory

SESSION: Verified Programming Tools

Verified compilation of CakeML to multiple machine-code targets

Complx: a verification framework for concurrent imperative programs

Verifying dynamic race detection

SESSION: Homotopy Type Theory

The HoTT library: a formalization of homotopy type theory in Coq

Lifting proof-relevant unification to higher dimensions

The next 700 syntactical models of type theory

SESSION: Formal Verification of Programming Language Foundations

Type-and-scope safe programs and their proofs

Formally verified differential dynamic logic

Equivalence of System F and λ2 in Coq based on context morphism lemmas