## 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 given this link

#### Contact(s)

### Next talk

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.

### Previous talks

#### Year 2019

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*