CPP 2016: THE FIFTH INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS
PROGRAM

Days: Monday, January 18th Tuesday, January 19th

Monday, January 18th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 1: Invited talk by Harvey Friedman

Invited talk by Harvey Friedman, Ohio State University

Title: Perspectives on Formal Verfication

Abstract: I will discuss the importance, uses, and future directions of formal verification from the point of view of a mathematical foundationalist. These include issues of certainty, proof structure, and (finitary) completeness and decidability.

10:30-12:00 Session 2: Verifying Imperative Programs

Verifying Imperative Programs

10:30
Higher-order Representation Predicates in Separation Logic ( abstract )
11:00
A Unified Coq Framework for Verifying C Programs with Floating-Point Computations ( abstract )
11:30
Refinement Based Verification of Imperative Data Structures ( abstract )
14:00-15:30 Session 3: Design and Implementation of Theorem Provers

Design and Implementation of Theorem Provers

14:00
The Vampire and the FOOL ( abstract )
14:30
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions ( abstract )
15:00
Mizar Environment for Isabelle ( abstract )
16:00-18:00 Session 4: Mathematics

Mathematics

16:00
A Modular, Efficient Formalisation of Real Algebraic Numbers ( abstract )
16:30
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials ( abstract )
17:00
Formalizing Jordan Normal Forms in Isabelle/HOL ( abstract )
17:30
Formalization of a Newton series representation of polynomials ( abstract )
Tuesday, January 19th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 5: Invited talk by Leonardo de Moura

Invited talk by Leonardo de Moura, Microsoft Research, Redmond

Title: Dependent Type Practice

Abstract: Dependent type theory is a powerful and expressive language for writing mathematical expressions and proofs, but careful design, engineering, and hard work are needed to put the theory into practice. In this talk, I will discuss some of the ideas and techniques that have been used in the design of the Lean theorem prover, a new proof system based on dependent type theory that aims to make the theorem proving process more natural, convenient, and efficient.

10:30-12:00 Session 6: Foundations

Foundations

10:30
A Logic of Proofs for Differential Dynamic Logic ( abstract )
11:00
Constructing the Propositional Truncation using Non-recursive HITs ( abstract )
11:30
A Nominal Exploration of Intuitionism ( abstract )
14:00-15:30 Session 7: Verification for Concurrent and Distributed Systems

Verification for Concurrent and Distributed Systems

14:00
Bisimulation Up-to Techniques for Psi-calculi ( abstract )
14:30
Planning for Change in a Formal Verification of the Raft Consensus Protocol ( abstract )
15:00
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules ( abstract )
16:00-17:00 Session 8: Compiler Verification

Compiler Verification

16:00
Formal Verification of Control-flow Graph Flattening ( abstract )
16:30
Axiomatic Semantics for Compiler Verification ( abstract )
18:00-21:00 Session

CPP Reception, sponsored by the DeepSpec project

The Science of Deep Specification is a new U.S. National Science Foundation initiative on applying proof assistants at scale to system verification.  Come learn about the project, with a brief presentation by Benjamin Pierce, plus, of course, plenty of food, drink, and socializing.