CPP 2016

The 5th ACM SIGPLAN Conference on

Certified Programs and Proofs

in cooperation with ACM SIGLOG

Saint Petersburg, Florida, USA - January 18-19, 2016

# CPP 2016 Accepted Papers

Refinement Based Verification of Imperative Data Structures

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

Planning for Change in a Formal Verification of the Raft Consensus Protocol

A Modular, Efficient Formalisation of Real Algebraic Numbers

Formalization of a Newton series representation of polynomials

Axiomatic Semantics for Compiler Verification

A Nominal Exploration of Intuitionism

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

A Unified Coq Framework for Verifying C Programs with Floating-Point Computations

Formal Verification of Control-flow Graph Flattening

Higher-order Representation Predicates in Separation Logic

Bisimulation Up-to Techniques for Psi-calculi

The Vampire and the FOOL

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

Mizar Environment for Isabelle

Formalizing Jordan Normal Forms in Isabelle/HOL

A Logic of Proofs for Differential Dynamic Logic

Constructing the Propositional Truncation using Non-recursive HITs