View: session 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 SPEAKER: unknown ABSTRACT. Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of self-driving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundness-critical and extra logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live deterministic programs from liveness proofs for nondeterministic programs. This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms -- syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions. |

11:00 | Constructing the Propositional Truncation using Non-recursive HITs SPEAKER: Floris van Doorn ABSTRACT. In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all results in a new proof assistant, Lean. |

11:30 | A Nominal Exploration of Intuitionism SPEAKER: unknown ABSTRACT. This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories a la Martin-Lof) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer's Continuity Principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's meta-theory using our formalization of Nuprl in Coq and show how we can reflect these meta-theoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key meta-theoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem and bar induction on monotone bars. |

**Verification for Concurrent and Distributed Systems**

**Compiler Verification**

**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.