European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

Programme

  Mon 24 Tue 25
09:30-10:30 Gratzer Mörtberg
10:30-11:10 break break
11:10-11:40 Uemura Møgelberg
11:40-12:10 Bradley Doré
12:10-14:10 lunch lunch
14:10-15:10 Pujet Lafont
15:10-15:50 break break
15:50-16:20 Nuyts Felicissimo
16:20-17:00 break break
17:00-17:30 Rasekh Moreau
17:30-18:00 Bocquet  

Invited talks

Daniel Gratzer (Aarhus University): Controlling unfolding in type theory

Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. We present a new system where definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our system by means of elaboration to a core theory with extension types—a connective first introduced in the context of HoTT—and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda.

Ambroise Lafont (University of Cambridge): Generic pattern unification: a categorical approach

We provide a generic categorical setting for Miller’s pattern unification. The syntax with metavariables is generated by a free monad applied to finite coproducts of representable functors; the most general unifier is computed as a coequaliser in the associated multisorted Lawvere theory. Our setting handles simply typed second-order syntax, linear syntax, or (intrinsic) polymorphic syntax such as system F. This is a joint work with Neel Krishnaswami.

Anders Mörtberg (Stockholm University): Computational proofs in Cubical Type Theories

In recent years we have been able to do a variety of proofs in synthetic homotopy theory purely by automatic computation in Cubical Agda, including the computation of a variation on the Brunerie number. These computations and proofs should be possible to carry out in other cubical systems, like cubicaltt, redtt, cooltt, etc. However, translating results between these systems can be quite challenging as the underlying cubical type theories are quite different. In the talk I will discuss various proofs by computation that we have done as well as some ideas on how to translate proofs between cubical type theories.

Loïc Pujet (INRIA): Mechanising reducibility proofs in Coq

Reducibility models play a central role in the metatheory of type theory: they are the starting point for all proofs of normalisation and decidability. But in the case of dependent type theories, reducibility models become complex and somewhat fragile, with many interdependent parts.

This complexity makes reducibility proofs an ideal candidate for formalisation. And indeed, the community has made significant efforts in that direction, notably with the Coq proof of Barras and Werner for the Calculus of Constructions, and the Agda proof of Abel, Öhman and Vezzosi for Martin-Löf Type Theory.

In this talk, I will report on an experiment to extend and mechanise in Coq the reducibility proof of Abel et al. In comparison to their development, ours attempts to minimise the gap between the theory and the necessary meta-theory, and pushes the verification all the way to a bidirectional type-checking algorithm.

Additionally, I will survey some exciting developments in the community that make use of reducibility models to tackle several open problems in type theory.

This talk is based on joint work with Arthur Adjedj, Meven Lennon-Bertrand and Kenji Maillard.

Contributed talks

Rafaël Bocquet (Eötvös Loránd University): For the Metatheory of Type Theory, Internal Sconing Is Enough

I will present results obtained in joint work with Ambrus Kaposi and Christian Sattler, written in the preprint arXiv:2302.05190.

Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization.

Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model.

Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity, normalization and syntactic parametricity for type theory.

Felix Bradley (Royal Holloway, University of London): On the Metatheory of Subtype Universes

Subtype universes were initially introduced by Maclean and Luo as a way of formulating the notion of a ‘type of subtypes’ for a logical type theory equipped with coercive subtyping. This extended type theory has several nice metatheoretical properties such as strong normalisation, but this implementation excluded certain kinds of subtyping relations from being used, and the formulation was wrapped up in the complexities of the underlying type theory’s universe hierarchy. We consider a simpler yet more expressive reformulation of subtype universes with the ability to extract coercions and discuss how this lifts the limits on what subtype relations can be used, and how the choice of subtype relations impacts the metatheory.

Maximilian Doré (University of Oxford): Automating reasoning in cubical type theory

Properties of Kan cubical sets are treated as logical rules in cubical type theory. The purpose of this talk is to study these rules from the point of view of automated reasoning. We establish NP-completeness for finding cells in a cubical set and undecidability of finding cells in a Kan cubical set with reductions to satisfiability checking and string rewriting, respectively. We present algorithms and heuristics to still find cells in many practical cases, and an experimental implementation of the findings in a tactic for Cubical Agda.

Thiago Felicissimo (Deducteam/LMF/Inria): A Logical Framework for Computational Theories with Minimal Syntax and Bidirectional Typing

Logical frameworks are important tools for unifying the study and implementation of type theories. In this talk I will introduce CompLF, a logical framework for computational theories. It aims at representing the syntax of theories in a faithful way, and one of the ways it achieves this is by supporting erased arguments. These are arguments that are part of the typing rules but are omitted from the syntax, allowing for example to write abs(x. t) instead of abs(A, x. B, x. t). Erased arguments enable us to define the syntax that we are used to, but make typechecking a non-trivial and in general undecidable task.

To address this problem, I propose a bidirectional typing algorithm for CompLF. Bidirectional typing complements erased arguments very well, as it allows to specify the flow of typing information in a way that makes clear the redundancy of such arguments. The main distinguishing feature of the algorithm is that it is theory agnostic: it can be instantiated with multiple theories, and by varying the amount of annotations in the syntax we also vary its amount of completeness.

Finally, CompLF is designed to be not only a theoretical tool but also a practical one: it has been implemented and can be found at https://github.com/thiagofelicissimo/complf.

Rasmus Møgelberg (IT University of Copenhagen): Higher Inductive Types in Coinductive Definitions via Guarded Recursion

Clocked Cubical Type Theory (CCTT) extends cubical type theory with multi-clocked guarded recursion. One of the intended applications of this is for programming with coinductive types, going beyond the standard examples of M-types that most previous work considers. For example, one can use higher inductive types in coinductive definitions as needed to e.g. describe non-deterministic or probabilistic processes. In this talk I will give an overview of CCTT, focussing on the constructions relevant for coinductive types. I hope to have time to also sketch the denotational semantics.

Vincent Moreau (IRIF, Université Paris Cité): Profinite lambda-terms and parametricity

This talk will present a definition of profinite lambda-terms of any simple type. Profinite structures naturally appear in automata theory as a way to speak about limiting behavior of finite words, giving rise to the notion of profinite word. At the same time, the Church encoding establishes a one-to-one correspondence between finite words and simply-typed lambda-terms, taken modulo beta and eta, of a type given by their finite alphabet. Our definition extends this correspondence between profinite lambda-terms of a Church type and profinite words over the associated alphabet. We start by introducing the set of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. We show that this resulting notion of profinite lambda-term, coming from Stone duality, lives in perfect harmony with the principles of Reynolds parametricity. Indeed, we prove a parametricity theorem for Church encodings of words, stating that every parametric family of elements in the finite standard model is the interpretation of a profinite lambda-term.

This is joint work with Sam van Gool and Paul-André Melliès, available at https://arxiv.org/abs/2301.12475.

Andreas Nuyts (KU Leuven): Every modality is a relative right adjoint

(J.w.w. Josselin Poiret) MTT (multimode type theory) is a type system that combines high generality (in the sense that it can be instantiated with a mode theory of one’s choice) with a relatively simple metatheory. The main complaint about the system is that it requires every internal modality to be a (weak) dependent right adjoint, with the lock operation on contexts interpreted by the left adjoint. In a way, this restriction is an immediate consequence of one of the design goals of MTT, namely that the user should not be asked for explicit substitutions and that there should be no delayed substitutions. This requires that every context should have a universal approximation as a context in the image of the modality, which is exactly what a left adjoint gives. It is therefore not easy to find a design space where the complaint can be addressed. This is why we think it is worthwhile to communicate an idea still in early development: Every functor F : C -> D is a relative right adjoint along the yoneda-embedding h : C -> Copsh(C) of C in its copresheaf category. This allows for an introduction rule for the modal type FT taking a subterm of type hT. While MTT modalities (being right adjoints) always respect limits, h never respects non-trivial limits; h thus acts as a guard for functors F that do not respect limits.

Nima Rasekh (Max Planck Institute for Mathematics): Category Theory of Universes

A key concept of higher topos involves the existence of universes, either by definition (in the elementary case) or by construction (in the Grothendieck case). In this talk we want to illustrate how the comprehending the category theory of internal universes can help us internalize a variety of key constructions.

Taichi Uemura (Stockholm University): Towards modular proof of normalization for type theories

I will present an idea of modular or compositional proof of normalization for type theories. Normalization is defined as a property of a morphism of type theories, and the class of morphisms satisfying normalization is closed under pushouts and composition. Normalization for a complex type theory is then a formal consequence of normalization for its smaller fragments.