CPP 2016- Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs

Full Citation in the ACM Digital Library

SESSION: Keynotes

Perspectives on formal verification (invited talk)

Dependent type practice (invited talk)

SESSION: Verifying Imperative Programs

Higher-order representation predicates in separation logic

A unified Coq framework for verifying C programs with floating-point computations

Refinement based verification of imperative data structures

SESSION: Design and Implementation of Theorem Provers

The vampire and the FOOL

Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions

Towards a Mizar environment for Isabelle: foundations and language

SESSION: Mathematics

A modular, efficient formalisation of real algebraic numbers

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials

Formalizing Jordan normal forms in Isabelle/HOL

Formalization of a Newton series representation of polynomials

SESSION: Foundations

A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

Constructing the propositional truncation using non-recursive HITs

A nominal exploration of intuitionism

SESSION: Verification for Concurrent and Distributed Systems

Bisimulation up-to techniques for psi-calculi

Planning for change in a formal verification of the raft consensus protocol

A verified algorithm for detecting conflicts in XACML access control rules

SESSION: Compiler Verification

Formal verification of control-flow graph flattening

Axiomatic semantics for compiler verification