## Type theory and realisability

#### Day, hour and place

Wednesday at 2pm, room 1007

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

### Previous talks

#### Year 2022

Type theory and realisability

Wednesday December 14, 2022, 2PM, Salle 1007

**Rémy Cerda** (Institut de Mathématiques de Marseille, Université Aix-Marseille) *To be announced.*

Type theory and realisability

Wednesday November 16, 2022, 2PM, Salle 1007

**Hugo Férée Et Sam Van Gool** *A formally verified construction of propositional quantifiers for intuitionistic logic*

In this talk, we will give some background for the result, and I will make some points about its proof that we clarified during its implementation, which also give some new insights about the “pen-and-paper” proof. In our implementation, as in Pitts' original proof, the propositional quantifiers are defined by a mutual induction based on Dyckhoff's proof calculus LJT. The correctness of the construction is then proved by an induction on the size of an LJT-proof. The techniques used and lessons learned from our implementation may also be of more general interest for verified implementations of other proof-theoretic results.

Type theory and realisability

Friday October 21, 2022, 10AM, Salle 1007

**Thorsten Altenkirch** *Do we need classical logic?*

Type theory and realisability

Wednesday October 19, 2022, 2PM, Salle 1007

**Peter Dybjer** *On Generalized Algebraic Theories and Categories with Families*

Also on https://galene.org:8443/group/herbelin/gt-rea-tt (no password)

Type theory and realisability

Wednesday October 19, 2022, 3:15PM, Salle 1007

**Ambrus Kaposi** *Formalisation of type theory in type theory using quotient-inductive-inductive-recursive types*

Also on https://galene.org:8443/group/herbelin/gt-rea-tt (no password)

Type theory and realisability

Wednesday October 12, 2022, 2PM, Salle 3052

**Félix Castro** *An interpretation (by parametricity) of E-HA^ω inside HA^ω*

In this talk, we will see how the study of a (family of) partial equivalence relation(s indexed by the sorts of System T) leads us to design a translation (by parametricity) from E-HA^ω (HA^ω + extensional equality at all level) to HA^ω (where equality is only defined on natural numbers).

Type theory and realisability

Wednesday July 6, 2022, 2PM, Salle 1007

**James Lipton** (Wesleyan Univ., USA) *CUT ELIMINATION in Higher-Order with (HO) constraints*

If constraints are unrestricted, cut-elimination is easily shown to fail, because of the way the system handles equality rules. Our work studies conditions on the constraint system C that guarantee cut-elimination. The techniques used are based on Takahashi, Prawitz ande Andrews' work in classical type theory, Lipton and DeMarco for intuitionistic type theory, with ideas developed by Hermant for Logique Modulo, Hermant and Lipton for Logic with sequent axioms, as well as cut-elimination techniques due to Okada and Maehara.

We will briefly discuss Kripke and HA semantics for these calculi, with some remarks on fibrational semantics developed by the speaker with Gianluca Amato (Pescara, Italy) if time permits!

This will be a blackboard talk (with maybe a few slides) and will include work in progress!

#### Year 2021

Type theory and realisability

Wednesday December 8, 2021, 2PM, Salle 1007

**Federico Olimpieri** (Université de Leeds) *Categorifying Intersection Types*

Type theory and realisability

Wednesday February 24, 2021, 2PM, online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)

**Elaine Pimentel** (UFRN - Brazil) *On linear logic, modalities and frameworks*

We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs.

We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic.

#### Year 2020

Type theory and realisability

Wednesday December 16, 2020, 2:30PM, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)

**Pierre Pradic** (University of Oxford) *Implicit automata in λ-calculi*

This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages.

After introducing and motivating the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide, I will discuss refinements we obtained for linear λ-calculi. I will focus on a correspondence with functions computed by copyless streaming string transducers (SSTs), and particularly on the ingredients of a completeness proof translating λ-terms to transducers. This will involve the notions of categorical automata as introduced by Colcombet and Petrisan, categorical models of linear logic and free completions, as well as automata-theoretic techniques related to the composition and determinization of SSTs.

Type theory and realisability

Monday December 14, 2020, 2PM, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)

**Armaël Guéneau** (Aarhus University) *Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code*

This work has been entirely mechanized in Coq using the Iris framework:

https://github.com/logsem/cerise https://github.com/logsem/cerise-stack

#### Year 2019

Type theory and realisability

Wednesday December 11, 2019, 2PM, Salle 1007

**Danny Gratzer** *Type Theory à la Mode*

Despite the wide variety of uses, a general framework for modal dependent type theories has still proven elusive. Each modal situation requires a handcrafted type theory, and establishing the properties of these type theories requires a significant technical investment.

In this work, we have attempted to isolate a class of modal situations which can be given a single uniform syntax and allow for the typical metatheorems of type theory to be proven once and for all. Our calculus takes a mode theory as a parameter (an abstract description of the collection of modes, the modalities between them, and the ways in which they interactions) and produces a full dependent type theory satisfying canonicity.

Our approach generalizes the ideas latent in Nuyts, Vezzosi, and Devriese, and simplifies the forthcoming work by Licata, Shulman, and Riley on a subset of mode theories. This calculus is sufficiently flexible to model internal parametricity, guarded recursion, and even axiomatic cohesion.

Type theory and realisability

Wednesday November 27, 2019, 2PM, Salle 1007

**Bas Spitters** (Aarhus university) *Synthetic topology in Homotopy Type Theory for probabilistic programming*

Joint work with Martin Bidlingmaier (Aarhus) and Florian Faissole (INRIA).

Type theory and realisability

Wednesday September 18, 2019, 2PM, Salle 1007

**Karl Palmskog** (The University of Texas at Austin) *mCoq: Mutation Proving for Analysis of Verification Projects*

Joint work with Ahmet Celik, Marinela Parovic, Emilio Jésus Gallego Arias, and Milos Gligoric.

Speaker bio: Karl Palmskog is a Research Fellow at The University of Texas at Austin. His research focuses on proof engineering techniques and verification of distributed systems using Coq. He was previously a postdoctoral researcher at University of Illinois at Urbana-Champaign, working on topics related to the actor model of message-passing concurrency. He obtained his PhD from KTH Royal Institute of Technology.

Video available at https://youtu.be/S6b6OMFiDFA Slides available at https://setoid.com/slides/irif-2019.pdf

Type theory and realisability

Friday May 24, 2019, 2PM, Salle 1007

**Hugo Moeneclaey** *Monoids up to Coherent Homotopy in Two-Level Type Theory*

Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy.

In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it.

References

1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094)

2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155)

Organisé conjointement avec le groupe de travail catégories supérieures, polygraphes, et homotopie.

Type theory and realisability

Friday March 29, 2019, 11AM, Salle 3052

**Emilio J. Gallego Arias** (MINES ParisTech) *Formalized Logic Programming, from Theory to Practice*

(Constraint) logic programming is based on the utilization of proof search as a device for computation. The power that such a paradigm offers often comes at a cost for formal language research and implementation. Logic variables, unification, renaming apart, and proof search strategies are cumbersome to handle formally, and often specified informally or at the meta-logical level.

In the first part of the talk I will describe algebraic semantics for proof search, based on the Tarski's relation algebras and Freyd's allegories. The main idea is to translate logic programs to _variable free_ relations; distribute relational algebras with quasi-projections do interpret defined predicates, whereas first-order rewriting simulates the traditional SLD proof search procedure.

While the relation-based approach suffices to capture the proof search in a complete way, some rewriting steps are unsatisfactory from a more operational point of view, as they introduce extraneous terms in order to preserve certain global constraints. In an attempt to remedy this, we switch to the categorical version of relation algebra: allegories.

In particular, for a signature Σ, we will interpret logic programs in the so-called Σ-allegories: distribute allegories whose conjunctive part is tabulated by a “Regular Lawvere Category”.

In this setting, the single primitive of relation composition emcompasses unification, garbage collection, parameter passing, and environment creation and destruction. Tabulations play a crucial role, with their domain representing the set of live existential variables. Proof search is carried out by a notion of diagram rewriting, and is complete w.r.t. SLD, and satisfactory as form of abstract syntax for the program's execution. This new semantics paves the way to a formal extension of CLP with useful programming constructs.

In the second part, I will shift focus to a different part of the logic programming spectrum, and describe ongoing efforts on formalizing logic programming engines over theories with finitary models on the Coq proof assistant. In particular, I will describe the implementation and verification of an engine for incremental model computation of a subset of Datalog that we have dubbed “Regular Datalog”.

“Regular” Datalog stems from [Reutter,Romero,Vardi] Regular Queries, and it is of interest to the graph database community. The finite nature of the semantics of such programs allows to handle them quite naturally inside a constructive proof assistant, and to remain close to the usual mathematical notation. Borrowing from techniques from incremental view maintenance, we have developed a verified incremental model construction engine; to achieve a cost-effective mechanized proof of the soundness of the engine we had to develop a few notions specific to the ITP domain, such as generalized program signatures and a notion of relative satisfaction. We provide some preliminary benchmarks of the verified engine over realistic scenarios.

To conclude, I will present some challenges that the practical utilization of proof assistants does face these days, and briefly discuss my ongoing work on this area.

#### Year 2018

Type theory and realisability

Friday May 18, 2018, 11AM, Salle 3052

**Raphaël Cauderlier** *Tactics and certificates in Meta Dedukti*

We use meta-programming to define a tactic language for the Dedukti logical framework which can be used both for checking certificates produced by automatic provers and for developing proofs interactively.

More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped tactic language built on top of the typed one. We show the expressivity of these languages on two applications: a transfer tactic and a resolution certificate checker.

Type theory and realisability

Wednesday April 25, 2018, 2PM, Salle 1007

**Hadrien Batmalle** (IRIF) *Préservation de propriétés du modèle de départ en réalisbilité classique*

Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ “raisonnable”, supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera un analogue des “conditions d'antichaîne” du forcing nous permettant d'exporter certaines propriétés du modèle de départ au modèle de réalisabilité; et on l'appliquera pour obtenir des programmes réalisant Non DC (resp. Non CH) à partir de modèles de ZF bien choisis validant Non DC (resp. Non CH).

— DC: axiome du choix dépendant CH: hypothèse du continu

Type theory and realisability

Monday March 19, 2018, 1:15PM, 3052

**Adrien Guatto** *A Generalized Modality for Recursion*

Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.

We integrate our modality into a typed λ-calculus. We equip this calculus with an operational semantics, as well as an adequate denotational semantics in the topos of trees, a standard categorical model for guarded recursion. Building on top of categorical ideas, we describe an abstract type-checking algorithm whose completeness entails the coherence of both semantics.

Attention, horaire et salle inhabituels

Type theory and realisability

Wednesday March 14, 2018, 2PM, Salle 1007

**Laura Fontanella** (Institut de Mathématiques de Marseille) *L'Axiome du Choix dans la réalisabilité classique*

Type theory and realisability

Wednesday February 14, 2018, 2PM, Salle 1007

**Jérôme Siméon** (Clause, Inc.) *Specifying and compiling domain specific languages using Coq: Three case studies*

We describe how each of those languages comes with its own challenges, and how they benefit differently from the use of a proof assistant. We also show how we could exploit their commonalities to build an optimizing and (partially) verified compiler for each of them. The core of that compiler uses traditional database representations (the Nested Relational Algebra and its corresponding Calculus) for optimization and code-generation.

– Some of this work was done jointly with Joshua Auerbach, Martin Hirzel, Louis Mandel and Avi Shinnar as part of the Q*cert project (https://querycert.github.io/).

Type theory and realisability

Wednesday January 31, 2018, 2PM, Salle 1007

**Armaël Guéneau** (Inria Paris) *A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification*

Type theory and realisability

Wednesday January 17, 2018, 2PM, Salle 1007

**Rodolphe Lepigre** *Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs*

References and links: - paper: http://lepigre.fr/files/docs/lepigre2017_subml.pdf - implementation of the system: https://github.com/rlepigre/subml - online interpreter and examples: https://rlepigre.github.io/subml

#### Year 2017

Type theory and realisability

Wednesday December 20, 2017, 2PM, Salle 1007

**Ludovic Patey** (ICJ, Lyon) *Introduction aux mathématiques à rebours*

Type theory and realisability

Wednesday December 6, 2017, 2PM, Salle 1007

**Francesco A. Genco** (IRIF - TU Wien) *Typing Parallelism and communication through hypersequents*

Type theory and realisability

Wednesday November 29, 2017, 2PM, Salle 1007

**Guilhem Jaber** (ENS Lyon) *A Trace Semantics for System F Parametric Polymorphism*

Type theory and realisability

Thursday March 16, 2017, 2PM, Salle 1007

**Pierre-Marie Pédrot** *An Effectful Way to Eliminate Addiction to Dependence*