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.

Overview — Social activities — Abstracts — Meeting homepage

Overview

All talks will take place in room 14, house 5, at Kräftriket (map).

Friday 20 May

Saturday 21 May

Social activities

The workshop dinner is 19:00 at Shahrzad, a classic Persian restaurant, 30mins walk from Kräftriket (or 10mins bus + 10 mins walk). We have a pre-booked set menu at 500kr/person (drinks not included), with alternatives available for dietary restrictions.

On Sunday, there will be an informal social excursion — not highly organised, mainly just a gathering-point to start off together. If the weather is nice, we will go to Skansen, an open-air museum of Swedish culture and history (entrance 200kr); if it’s rainy we’ll go to Moderna Museet/ArkDes, a museum of modern art, architecture, and design (main collections free entry, some exhibitions charge entry). Both options have good cafés for lunch/snacks, and other sightseeing nearby. In either case, this is; meet at 11:00 at the main entrance (of Skansen or Moderna Museet), and take things informally from there. We’ll announce which it is on Saturday evening!

Abstracts

Friday 20 May

9.30–10.30: Jonathan Sterling (Aarhus University), Naïve logical relations in synthetic Tait computability

Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos’ book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists.

10.50–11.10: Steve Awodey (Carnegie Mellon University), Kripke-Joyal forcing for Martin-Löf type theory • slides

I will report on recent joint work with Nicola Gambino and Sina Hazratpour, generalizing the Kripke-Joyal forcing semantics of topos theory from IFOL and IHOL to MLTT, contained in the paper arXiv:2110.14576.

11.10–11.30: Niels Van der Weide (Radboud University), Semantics for two-dimensional type theory • slides

In this work, we propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

11.30–11.50: David Wärn (University of Gothenburg), Effective quotients in homotopy type theory

For a type X, one expects that surjections from X correspond to ‘higher equivalence relations’ on X. A priori this idea is difficult to express internally to type theory since it involves an infinite tower of coherences. In this talk, we give an internal definition of higher equivalence relations and show it to be equivalent to surjections out of X. As an application we obtain a simple proof of the stabilisation theorem for higher groups.

11.50–12.10: Roussanka Loukanova (Bulgarian Academy of Sciences), Syntax-Semantics of Simply Typed Theory of Acyclic Algorithms (cancelled)

In 1989, Moschovakis [1] initiated a new theory of the mathematical notion of algorithm, within untyped, full recursion. In 2006, Moschovakis [2] introduced the formal language of higher-order Type-Theory of Acyclic Algorithms (TTAR) via simple types, which models the notion of algorithm and concepts of meaning in simply-typed semantic structures. The focus of [2] is on computations that end up after finite number of steps. The approach, in its varieties, with full and acyclic recursion, provides for new developments of type theory of computation and new applications to computational syntax-semantics interfaces in programming and natural languages.

In this talk, I present the formal language (LAR) of TTAR, by extending it with a restrictor operator that sets conditions on denotations of terms. In addition, the operator defines restricted memory and parameters. TTAR provides two kinds of semantics of the formal language LAR, denotational and algorithmic. The reduction system of TTAR is essential for the notion of algorithm and syntax-semantics interfaces. I shall overview the reduction calculus and some of the theoretical results of TTAR.

  1. Yiannis N Moschovakis. The formal language of recursion. Journal of Symbolic Logic, 54(04):1216–1252, 1989.
  2. Yiannis N. Moschovakis. A Logical Calculus of Meaning and Synonymy. Linguistics and Philosophy, 29(1):27–89, 2006.

13.40–14.40: Andrej Bauer (University of Ljubljana), One syntax to rule them all • blog post & formalisation

The raw syntax of a type theory, or more generally of a formal system with binding constructs, involves not only free and bound variables, but also meta-variables, which feature in inference rules. Each notion of variable has an associated notion of substitution. A syntactic translation from one type theory to another brings in one more level of substitutions, this time mapping type-theoretic constructors to terms. Working with three levels of substitution, each depending on the previous one, is cumbersome and repetitive. One gets the feeling that there should be a better way to deal with syntax.

In this talk I will present a relative monad capturing higher-rank syntax which takes care of all notions of substitution and binding-preserving syntactic transformations in one fell swoop. The categorical structure of the monad corresponds precisely to the desirable syntactic properties of binding and substitution. Special cases of syntax, such as ordinary first-order variables, or second-order syntax with variables and meta-variables, are obtained easily by precomposition of the relative monad with a suitable inclusion of restricted variable contexts into the general ones. The meta-theoretic properties of syntax transfer along the inclusion.

The relative monad is sufficiently expressive to give a notion of intrinsic syntax for simply typed theories. It remains to be seen how one could refine the monad to account for intrinsic syntax of dependent type theories.

This is joint work with Danel Ahman from the University of Ljubljana.

14.40–15.00: Maximilian Doré (University of Oxford), Automating Kan composition • slides

Cubical type theory offers a new of conducting topological arguments with its built-in Kan composition. Constructing a cube with Kan composition amounts to constructing a higher cube with appropriate boundaries, which is a very combinatorial task amenable to automation. In this talk I want to discuss recent work on doing this with the well-known algorithmic technique of constraint satisfaction. If we want to construct an n-dimensional cube as the top lid of a (n+1)-dimensional cube, we can solve a constraint satisfaction problem (CSP) with 2n+1 variables, the domains of which are all n-cubes which have a boundary matching with the lid. The constraints represent that the boundaries of all faces of the cube must align with each other. The CSP can be solved efficiently in Haskell by employing monadic constraint solving, which also gives an elegant interface to employ different search strategies. In the future I hope to adapt this approach to all flavours of cubical type theory, to derive more involved arguments solving several mutually dependent goals at once, and to derive counterexamples to errant goals.

A highly experimental implementation of the solver can be found at https://github.com/maxdore/csolver. Eventual goal is to provide a tactic or internal implementation in Cubical Agda akin to Agsy.

15.00–15.20: Kenji Maillard (Inria Rennes - Bretagne Atlantique), The multiverse — Logical modularity for proof assistants

(J.w.w. Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau and Éric Tanter.)

Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class functions, type polymorphism and modules. As logical systems, however, modularity is lacking, and understandably so: incompatible reasoning principles — such as univalence and uniqueness of identity proofs — can indirectly lead to logical inconsistency when used in a given development, even when they appear to be confined to different modules. The lack of logical modularity in proof assistants also hinders the adoption of richer programming constructs, such as effects. In this talk, I will describe a general type-theoretic approach called the multiverse to endow proof assistants with logical modularity. The multiverse consists of multiple universe hierarchies that statically describe the reasoning principles and effects available to define a term at a given type. We identify sufficient conditions for this structuring to modularly ensure that incompatible principles do not interfere, and to locally restrict the power of dependent elimination when necessary. This extensible approach generalizes the ad-hoc treatment of the sort of propositions in the Coq proof assistant.

15.50–16.10: Iosif Petrakis (Ludwig-Maximilians-Universität München), Positive negation in constructive mathematics • slides

In standard constructive logic negation is treated as in classical logic in a negativistic and weak way. This is in contrast to the use of a positive and strong “or” and “exists”. In constructive mathematics however, we often find a positive and strong approach to negatively defined concepts, like that of inequality. This fact motivates a clear distinction between a positive and strong negation and the standard weak negation. Bringing together older ideas of Griss and Nelson and recent work of Shulman and ours, we investigate the role of a positive and strong negation in Bishop-style constructive mathematics.

16.10–16.30: Raffael Stenzel (Masaryk University), Higher geometric sheaf theories • slides

The theory of classifying toposes is a crucial feature of what makes the Elephant what it is: A powerful environment for varying mathematical expressions of related ideas to converge to a single concept. Particularly, it allows to manage the intricate world of continuously varying algebraic structures over topological spaces by way of the thoroughly organized syntax of symbolic logic.

As of yet, an according theory of classifying infinity-toposes has not been developed for various obstructive reasons. With this ultimate goal in mind, in this talk I propose a canonical sheaf theory for geometric infinity-categories; here, the notion of geometric infinity-category generalizes Anel and Joyal’s definition of infinity-logoi in straight-forward fashion. I do so by moving away from the classical sheaf condition over topological spaces — and over geometric categories more generally — and introduce a stronger limit- preserving property instead. We will see that the according higher geometric sheaves differ from the ordinary ones only by a subtle cotopological fragment. Yet it turns out that this fragment is crucial in various aspects. As a case in point, I show that every infinity-topos is the theory of higher geometric sheaves over itself, and that the same is generally not true for the ordinary geometric sheaves over itself.

Concerning this workshop, I would be particularly interested in discussions on whether or not the associated higher covers are the right way to think about — and eventually obtain — a notion of geometric HoTT’s, in such a way that these higher geometric sheaf theories present classifying infinity-toposes for them.

16.30–17.30: Anja Petković Komel (TU Wien), The essence of elaboration • slides

When using type theories in proof assistants the full syntax can quickly become too verbose to handle. One common solution to this problem is to design two type theories: a fully annotated type theory which has good meta-theoretic properties, is suitable for algorithmic processing and resides in the kernel of the proof assistant, and an economic one for the users’ input. The two theories are linked by elaboration, a reconstruction of missing information that happens during, or in parallel with, type-checking.

In this talk we will take a look at the type-theoretic account of an elaboration map: a section of a “forgetful” type-theoretic transformation $r : S \to T$ from the fully annotated type theory S, which we will call standard type theory, to the economic one T, called a finitary type theory. This definition of elaboration map enjoys two important meta-theoretic properties: every finitary type theory has an elaboration map to a standard type theory and it satisfies a universal property, making it unique up-to judgemental equality. We will also consider algorithmic aspects of elaboration and relate it to type-checking.

This is joint work with Andrej Bauer.

Saturday 21 May

10.00–11.00: András Kovács (Eötvös Loránd University), Type-theoretic signatures for algebraic theories and inductive types • slides

In the context of proof assistants, inductive types are specified by signatures of certain syntactic schemata. More generally, algebraic theories can be likewise specified by syntactic signatures. I present several type theories (“theories of signatures”) where certain closed types can be viewed as algebraic/inductive signatures. By varying available type formers, we can describe various classes of algebraic theories, ranging from single-sorted finite product theories to higher inductive-inductive theories. The type theories of signatures can be modeled in various categories of algebras; for instance, we can interpret a quotient inductive signature as an 1-category of algebras, and a higher inductive-inductive signature as a higher category. Thus, theories of signatures can be viewed as very simple directed type theories, where variance issues are avoided by disallowing higher-order functions. I also describe term algebra constructions: this means constructing initial algebras from syntactic terms of theories of signatures. This can be used as an intermediate step in reducing large classes of inductive types to basic type formers.

11.20–12.20: Théo Winterhalter (Max Planck Institute for Security and Privacy (MPI-SP)), MetaCoq: Sound and complete type checking for Coq, in Coq • slides

Coq is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the meta-theory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq.

With MetaCoq we offer both a formal specification of the meta-theory of Coq (currently excluding η-laws, modules, strict propositions and template polymorphism) and an implementation of a type checker that we prove correct and complete with respect to this specification. In order to do this, we have to prove several meta-theoretic properties such as confluence of the reduction or subject reduction, and rely on the axiom of strong normalisation.

I will mostly focus on the type checker and the meta-theory of Coq developed as part of the MetaCoq project lead by Matthieu Sozeau and including Jakob Botsch Nielsen, Simon Boulier, Yannick Forster, Meven Lennon-Bertrand and Nicolas Tabareau.

14.00–15.00: Taichi Uemura (University of Stockholm), Normalization for initial space-valued models of type theories • slides

Given a type theory, one can construct its initial set-valued model but also its initial space-valued model. The coherence problem asks if the initial space-valued model is actually set-valued. If this is the case, then the initial set-valued model admits a unique morphism to an arbitrary space-valued model, which allows us to interpret the type theory in higher structures.

We develop a normalization technique for the initial space-valued model to solve the coherence problem. Once we have proved that every type or term in the initial space-valued model has a unique normal form, calculation of the path spaces of the initial space-valued model is reduced to calculation of the path spaces between normal forms. The space of normal forms is defined as an (non-higher) inductive type in a certain ∞-topos, so its path spaces are easy to calculate.

Our normalization technique is a higher-dimensional version of normalization by evaluation. This is possible thanks to Bocquet, Kaposi, and Sattler’s relative induction principle and Sterling’s synthetic Tait computability. The relative induction principle gives us a definition of the category of renamings suitable for ∞-categorical generalization. The idea of synthetic Tait computability is to use extensional type theory as an internal language for glued 1-topoi to construct logical predicates. Its higher analogue is to use homotopy type theory as an internal language for glued ∞-topoi to construct logical predicates.

15.00–15.20: Jonas Frey (Carnegie Mellon University), Characterizing clan-algebraic categories • slides

Clans [2] provide a categorical notion of dependent algebraic theory that can be seen as syntax-free abstraction of Cartmell’s generalized algebraic theories and as such is closely related to concepts like contextual categories and categories with families. Viewed as algebraic theories, clans are equally expressive as finite-limit theories but contain more information: the same finite-limit theory can have representations by different clans, and in particular different clans can have the same category of Set-models. The additional information encoded in a clan T gives rise to a weak factorization system (E,F) on the locally finitely presentable category Mod(T) (first considered by Henry), from which the clan can be reconstructed up to Morita equivalence.

In this talk I will present a bi-equivalence between a 2-category of clans, and a 2-category of “clan-algebraic categories”: these are locally finitely presentable categories equipped with a weak factorization system satisfying an exactness condition. This characterization of clan-algebraic categories can be seen as a generalization of the characterization of algebraic categories as “exact cocomplete categories that are generated by perfectly presentable objects” given in [1].

  1. Adámek, Jiří, Jiří Rosický, and Enrico Maria Vitale. Algebraic theories: a categorical introduction to general algebra. Vol. 184. Cambridge University Press, 2010.
  2. Joyal, André. Notes on clans and tribes. arXiv preprint arXiv:1710.10238 (2017).

15.20–15.40: Jacopo Emmenegger, B-systems and C-systems are equivalent • slides

C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality theorem for type theories. I will speak about a joint work with Benedikt Ahrens, Paige Randall North and Egbert Rijke where we prove Voevodsky’s conjecture that the categories of B-systems and of C-systems are equivalent. We do so by specialising a more general equivalence between non-stratified versions of B-systems and C-systems, which we name E-systems and CE-systems, respectively.

16.00–16.20: Sergei Soloviev (IRIT, University of Toulouse), Consequences of Computational Asymmetry in Verifier-Falsifier Games • slides

Originally, Game Theoretic Semantics (GTS) was developed as a variant of verification procedure for already existing logical semantics. These semantics could be classical, constructive etc. I explore (or, rather, start the exploration) of how the GTS may be modified, or even “perversed”, if there are significant differences in the computational power of players. More recent works on GTS for type theories are viewed in this context.

References related to this talk:

  • Thierry Coquand “A Semantics of Evidence for Classical Arithmetic” (1995)
  • J.-L. Krivine “Dependent choice, ‘quote’ and the clock” (2003)
  • Denis Bonnay “Preuves et jeux sémantiques” (2004)
  • Boyer and Sandu “Between Proof and Truth” (2012)
  • Yamada “Game Semantics of Martin-Löf Type Theory” (2013), Odintsov, Speranski
  • Shevchenko “Hintikka’s Independence-Friendly Logic Meets Nelson’s Realizability” (2018)

16.20–16.40: Henning Basold (Leiden University), Towards behavioural types as coalgebras • slides

Category theoretical approaches have been fruitful in the investigation of type theories and their syntax, but typically syntax is treated inductively via algebras. In this talk, I would like to discuss how session types and context-free session types can be approached via coalgebras, which allows us to handle elegantly problems via coalgebraic techniques that purely syntactic approaches render more opaque. Using coalgebra to deal with the syntax of session types may lead the way to a coinductive treatment of general behavioural types and the corresponding logics.

16.40–17.40: Ivan Di Liberti (University of Stockholm), Bi-presentable 2-categories and (bilex) 2-sketches

Motivated by the study of several 2-categories of (first order) theories (Lex, Reg, Coh, Ex, Ext), we introduce bipresentable 2-categories and show that those provide a solid framework to develop semantics for 2-sketches, and in general describe 2-categories of theories. We define bi-accessible and bipresentable 2-categories in terms of bicompact objects and bifiltered bicolimits. We prove a bi-accessible right bi-adjoint functor theorem and deduce a 2-dimensional Gabriel-Ulmer duality relating small bilex 2-categories and finitely bipresentable 2-categories. Finally, we show that 2-categories of pseudo-algebras of finitary 2-monads on Cat are finitely bipresentable, which in particular captures the case of Lex, the 2-category of small lex categories. Invoking the technology of lex-colimits, we prove further that several 2-categories arising in categorical logic (Reg, Ex, Coh, Ext, Adh, Pretop) are also finitely bipresentable.