Automated Reasoning

Homotopy Type Theory and Univalent Foundations,

Selected Extended Papers of ITP 2017,

The James Construction and $$\pi _4(\mathbb {S}^{3})$$ π 4 ( S 3 ) in Homotopy Type Theory Abstract In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda code looks like, and we explain several techniques that we used in the formalization. In the second part, we use the James construction to give a constructive proof that \(\pi _4(\mathbb {S}^{3})\) is of the form \(\mathbb {Z}/n\mathbb {Z}\) (but we do not compute the n here).

CompCertS : A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics Abstract The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert compiler, albeit with a stronger formal guarantee: it gives a semantics to more programs and ensures that the memory consumption is preserved by the compiler. CompCertS is based on an enhanced memory model where, unlike CompCert but like Gcc, the binary representation of pointers can be manipulated much like integers and where, unlike CompCert, allocation may fail if no memory is available. The whole proof of CompCertS is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.

A Verified Generational Garbage Collector for CakeML Abstract This paper presents the verification of a generational copying garbage collector for the CakeML runtime system. The proof is split into an algorithm proof and an implementation proof. The algorithm proof follows the structure of the informal intuition for the generational collector’s correctness, namely, a partial collection cycle in a generational collector is the same as running a full collection on part of the heap, if one views pointers to old data as non-pointers. We present a pragmatic way of dealing with ML-style mutable state, such as references and arrays, in the proofs. The development has been fully integrated into the in-logic bootstrapped CakeML compiler, which now includes command-line arguments that allow configuration of the generational collector. All proofs were carried out in the HOL4 theorem prover.

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2 Abstract We present a new framework for formalizing mathematics in untyped set theory using auto2. We demonstrate that many difficulties with using set theory for formalization of mathematics can be addressed by improvements to automation, without sacrificing the inherent flexibility of the logic. As applications, we formalize in Isabelle/FOL the entire chain of development from the axioms of set theory to the definition of the fundamental group of an arbitrary topological space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.

Canonicity for Cubical Type Theory Abstract Cubical type theory is an extension of Martin-Löf type theory recently proposed by Cohen, Coquand, Mörtberg, and the author which allows for direct manipulation of n-dimensional cubes and where Voevodsky’s Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory Abstract We formalise second-order ZF set theory in the dependent type theory of Coq. Assuming excluded middle, we prove Zermelo’s embedding theorem for models, categoricity in all cardinalities, and the categoricity of extended axiomatisations fixing the number of Grothendieck universes. These results are based on an inductive definition of the cumulative hierarchy eliminating the need for ordinals and set-theoretic transfinite recursion. Following Aczel’s sets-as-trees interpretation, we give a concise construction of an intensional model of second-order ZF with a weakened replacement axiom. Whereas this construction depends on no additional logical axioms, we obtain intensional and extensional models with full replacement assuming a description operator for trees and a weak form of proof irrelevance. In fact, these assumptions yield large models with n Grothendieck universes for every number n.

Effect Polymorphism in Higher-Order Logic (Proof Pearl) Abstract The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. I show that if a monad is restricted to values of a fixed type, this notion can be formalised in HOL. Based on this idea, I develop a library of effect specifications and implementations of monads and monad transformers. Hence, I can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. I illustrate the usefulness of effect polymorphism with a monadic interpreter.

Guarded Cubical Type Theory Abstract This paper improves the treatment of equality in guarded dependent type theory ( \(\mathsf {GDTT}\) ), by combining it with cubical type theory ( \(\mathsf {CTT}\) ). \(\mathsf {GDTT}\) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement \(\mathsf {GDTT}\) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. \(\mathsf {CTT}\) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. \(\mathsf {CTT}\) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ( \(\mathsf {GCTT}\) ), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of \(\mathsf {CTT}\) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that \(\mathsf {CTT}\) can be given semantics in presheaves on \(\mathcal {C}\times \mathbb {D}\) , where \(\mathcal {C}\) is the cube category, and \(\mathbb {D}\) is any small category with an initial object. We then show that the category of presheaves on \(\mathcal {C}\times \omega \) provides semantics for \(\mathsf {GCTT}\) .