Abstract: Formalizing syntax and substitution is often the first step towards a formally verified proof assistant. Many non-trivial properties about substitution are typically required. For a language with many term constructors, e.g. Nuprl, proofs about substitution typically need similar reasoning across many cases. Therefore, while formalizing Nuprl, we used Howe's uniform representation of terms, which allowed us to consider only 3 cases while defining concepts like substitution and free variables, and proving properties about them. Extending the language with new constructs required absolutely no change in our thousands of lines of proofs about substitution, free variables, and alpha equality. Inspired by this robustness, we have created a library by generalizing our proofs to work for a large class of languages. One can specify a language as a collection of term constructors and their variable-binding signatures, and use our rich collection of proofs. We have recently used this library for proofs about the Certicoq compiler for Coq.
Abstract: UniMath, short for "Univalent Mathematics", refers to both a language (a.k.a. a formal system) for mathematics, as well as to a computer-checked library of mathematics formalized in that system. The UniMath library, under active development, aims to coherently integrate machine-checked proofs of mathematical results from many different branches of mathematics. The UniMath language is a dependent type theory, augmented by the univalence axiom. One goal is to keep the language as small as possible, to ease verification of the theory. In particular, general inductive types are not part of the language. In joint work with Mörtberg, we partially remedy this lack by constructing a class of inductive (families of) sets. This involves a formalization of a standard category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the inductive sets thus obtained. By combining the present work with a previous formalization of substitution systems by Ahrens and Matthes, we obtain a framework for specifying, via a signature, programming languages with binders as nested inductive datatypes. The datatypes are automatically equipped with the structure of a monad, where the monadic operations and axioms correspond to a well-behaved substitution operation.
Abstract: We develop a version of cubical Type Theory which is based on heterogenous logical relations with the view towards implementing Homotopy Type Theory. We compare our approach with the work by Coquand et al who have proposed a cubical type theory using the interval. This is based on joint work with Ambrus Kaposi.
Abstract: What is a mathematical mistake? Which mistakes can be detected by using proof assistants and which ones cannot? We discuss various types of mistakes, in definitions, theorems, proofs, as well as in axioms. We make an attempt at qualifying how serious certain types of mistakes are and which role formalization can play in detecting them.
Abstract: We present a new experimental feature of Agda, developed by Jesper Cockx, which allows the user to add custom rewrite rules to Agda. We show how such rewrite rules can be used to implement higher inductive types and can make univalence compute in some particular cases.
Abstract: One type theory may serve as a meta theory for another and we build a model of the target type theory in its meta theory. This gives us a relative consistency theorem. Moreover, when we use only constructive methods in the meta theory we obtain a constructive interpretation of the target type theory. We are carrying out such a project to get a constructive model of the Cubical Type Theory of Coquand et.al. which satisfies the Univalence Axiom. The model is a constructive presheaf model over a base category in which the objects are finite sets of names, I, J, and an arrow, I -> J is function from J to dM(I), the free DeMorgan algebra generated by I. To make this construction or, in general any presheaf model, it seems that we must reason extensionally as in set theory. This is difficult in an intensional type theory like Coq, but Nuprl's extensional constructive type theory gives us the flexibility we need. Since we have built a model of Nuprl in Coq, the constructive interpretation of Cubical Type Theory with Univalence is therefore built in two steps. First build Nuprl in Coq to get a good extensional theory, and then use that theory to get a univalent theory. Univalence follows from the existence of uniform composition structure for all types in the new theory, including a special Glue type. We have proved the equivalence of two different definitions of composition structure, and shown that they exist for the Pi, Sigma, and Path types. By the time of this meeting, we expect that composition for Glue, composition for Universe, and Univalence will all be verified.
Abstract: The HoTT/HoTT library is one of the major Coq libraries exploring univalent foundations and homotopy type theory, the other being UniMath. The library includes formalization of the basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions, and quotients, a formalization of modalities (reflective subtoposes) using modules as a way to quantify over all universe levels, formalizations of Cantor spaces and the surreals, the basic theory of h-levels, and a significant amount of category theory centered around comma categories and functoriality of various constructions involving comma categories. A significant amount of work has gone into ensuring that the library compiles quickly. This talk will discuss the various constructions in the HoTT library, as well as the design choices and features, both of Coq and of univalent type theory, which allow our library to compile and typecheck quickly.
Abstract: The UniMath library is a Coq library which aims to formalize mathematics using the univalent point of view. For this purpose, it is important to include a formalization of real numbers. As non-negative real numbers are used in many applications such as metric and normed spaces, I decided to formalize them first and then use this definition to define all real numbers. Using the existing formalization of subtypes in UniMath, I was able to provide a definition of non-negative real numbers inspired by Dedekind cuts and to prove all of the expected properties of the resulting constructive field of real numbers.
Abstract: Cubical type theory is an extension of dependent type theory which allows to directly reason about n-dimensional cubes (points, lines, squares, cubes etc.). It is based on a model of type theory in cubical sets given in a constructive metatheory. The type theory allows for new ways to reason about identity types, e.g., function extensionality as well as Voevodsky's univalence axiom are provable. We have impemented an experimental proof assistant based on this type theory called cubicaltt. In the talk I will discuss various examples that we have formalized in cubicaltt which uses that univalence computes.
Abstract: Nuprl is an interactive theorem prover that implements an extensional constructive type theory. Its types are interpreted as partial equivalence relations (PERs) on closed terms. Nuprl is both computationally and type-theoretically open-ended in the sense that both its computation system and its type theory can be extended as needed by checking a handful of conditions. For example, Doug Howe characterized the computations that can be added to Nuprl in order to preserve its key properties such as the congruence of its computational equivalence relation. We have implemented Nuprl's computation and type system in Coq, and we have showed among other things that it is consistent by (1) proving the validity of its inference rules w.r.t. its PER semantics, and (2) that False is uninhabited. Using our Coq framework we can now easily add new computations and types to Nuprl by mechanically verifying that all the necessary conditions still hold. For example, we have recently added nominal features to Nuprl in order to prove a version of Brouwer's continuity principle, as well as choice sequences in order to prove truncated versions of the axiom of choice and of Brouwer's bar induction principle.
Abstract: Coq is a general purpose proof assistant used for the formalization of mathematics and computer science. It can be used to formalize large results in the context of univalent foundations and homotopy type theory, as witnessed by the UniMath and HoTT/HoTT libraries. However, Coq is naturally geared towards working with an identity type living in the propositional sort Prop, possibly enjoying uniqueness of identity proofs. Moving towards a proof relevant identity type and universe polymorphic constructions requires important changes in low-level and high-level aspects of the system, from design choices for universe handling to tools for generalized rewriting and dependent pattern-matching, whose meaning changes slightly. I will describe the impact it had on these tools, the design choices made and the applications of these tools in univalent formalizations.
Abstract: Lean is a new proof assistant which is designed to support Homotopy Type Theory. Lean has a built-in HoTT library, which contains a solid foundation for doing HoTT, including most theorems from the HoTT book. In addition, the library contains category theory and there is active development in synthetic homotopy theory.
Abstract: Lean is a new open source dependently typed theorem prover which is mainly being developed by Leonardo de Moura at Microsoft Research. It is suited to be used for proof irrelevant reasoning as well as for proof relevant, univalent formalizations of mathematics. In my talk, I will present the experiences I had doing a formalization project in Lean. One of the interesting aspects of homotopy type theory is the ability to perform synthetic homotopy theory on higher types. While for the first homotopy group the choice of a suitable algebraic structure to capture the homotopic information is obvious -- it's a group -- implementing a structure to capture the information about both the first and the second homotopy group (or groupoid) of a type and their interactions is more involved. Following Ronald Brown's book on Nonabelian Algebraic Topology, I formalized two structures: Double groupoids with thin structures and crossed modules on groupoids. I furthermore attempted to prove their equivalence. The project can be seen as a usability and performance test for the new theorem prover.