Days: Monday, January 18th Tuesday, January 19th
View this program: with abstractssession overviewtalk overview
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.
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 ) |
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 ) |
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 ) |
View this program: with abstractssession overviewtalk overview
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.
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 ) |
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 ) |
Compiler Verification
16:00 | Formal Verification of Control-flow Graph Flattening ( abstract ) |
16:30 | Axiomatic Semantics for Compiler Verification ( abstract ) |
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.