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)


Previous talks



Year 2019

Type theory and realisability
Friday May 24, 2019, 2PM, Salle 1007
Hugo Moeneclaey Monoids up to Coherent Homotopy in Two-Level Type Theory

When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2].

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

I will present past and ongoing work to develop mechanically-verified semantics and implementations of constraint logic programming.

(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

Tactics are often featured in proof assistants to simplify the interactive development of proofs by allowing domain-specific automation. Moreover, tactics are also helpful to check the output of automatic theorem provers because they can rebuild details that the provers omit.

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

La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines…) axiomatisés au moyen d'algèbres de réalisabilité. Elle produit ainsi des modèles de ces théories, de même qu'une technique bien connue, le forcing de Cohen, dont elle est en fait une généralisation.

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

Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infnite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale.

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

La réalisabilité fournit une interpretation des formules d'un système logique (ou d'une théorie) dans un modèle de calcul. Introduite par Kleene dans les années `40, la réalisabilité est née comme une interprétation des formules de l'arithmétique de Heyting par des ensembles d'indices de fonctions récursives. Avec J.-L. Krivine, la recherche en réalisabilité a évolué jusqu’à englober les axiomes de la théorie des ensembles. Les techniques développées par Krivine fournissent une méthode pour construire des modèles de la théorie des ensembles où tout énoncé de la théorie ZF plus l'Axiome du Choix Dépendant est réalisé. L'Axiome du Choix Dépendant, DC, est une version faible de l'Axiome du Choix; si et comment il serait possible de réaliser l'Axiome du Choix dans sa totalité reste une question ouverte. Nous allons considérer des principes intermédiaires: (1) le principe de partition, PP : étant donné deux ensembles A et B, s’il y a une surjection de A dans B, alors il y a une injection de B dans A; (2) le “Dual Cantor Bernstein theorem”, CB* : s’il y a une surjection de A dans B et une surjection de B dans A, alors A et B sont équipotents; (3) le principe de partition faible, WPP : s’il y a une surjection de A dans B et une injection de A dans B, alors A et B sont équipotents. Ces principes découlent de l'Axiome du Choix et sont plus forts que l'Axiome du Choix Dépendant. Cependant, on ne sait pas s'ils sont équivalents à l'Axiome du Choix et cela est un vieux problème ouvert formulé par B. Banacschewski et G. Moore en 1990. Est-il possible de construire un modèle de réalisabilité pour l'un de ces principes? Cette recherche peut aboutir à deux situations divergentes: soit on trouvera des modèles de réalisabilité pour ces principes où l’axiome du choix est également réalisé, soit on s’arrêtera à une étape donnée sur des modèles de réalisabilité où l’un de ces principes (ou tous) est réalisé, tandis que l’Axiome du Choix ne l’est pas, dans ce dernier cas on aurait alors montré que ces principes ne sont pas équivalents à l’Axiome du Choix et on aurait ainsi résolu le problème de Banacschewski-Moore. Je vous presenterai l'avancement de mes recherches dans ce domaine.

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

Domain specific languages (DSL) can be well suited for certain business scenarios and be easier to learn for non-developers. We present our experience using the Coq proof assistant to support the formal specification and the compilation for three different DSLs: JRules (a language for business rules), SQL (a language for relational databases), and Jura (a language for legal contract).

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

I will present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. The framework is built on top of Separation Logic with Time Credits, embedded in the Coq proof assistant. I will formalize the O notation, which is key to enabling modular specifications and proofs, and cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. I will propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.

Type theory and realisability
Wednesday January 17, 2018, 2PM, Salle 1007
Rodolphe Lepigre Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs

In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion.

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

Les mathématiques à rebours sont un domaine fondationnel qui vise à trouver les axiomes optimaux pour prouver les théorèmes de la vie de tous les jours. Elles se placent dans l'arithmétique du second ordre, avec une théorie de base, RCA, capturant informellement les “mathématiques calculables”. Nous reviendrons sur les justifications historiques des mathématiques à rebours, présenterons ses principales observations, ainsi que l'approche moderne des mathématiques à rebours comme formalisme de classification de phénomènes calculatoires.

Type theory and realisability
Wednesday December 6, 2017, 2PM, Salle 1007
Francesco A. Genco (IRIF - TU Wien) Typing Parallelism and communication through hypersequents

We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. We discuss a normalisation procedure and several features of the parallel λ-calculus. Following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we also discuss the generalisation of the employed techniques for other intermediate logics.

Type theory and realisability
Wednesday November 29, 2017, 2PM, Salle 1007
Guilhem Jaber (ENS Lyon) A Trace Semantics for System F Parametric Polymorphism

In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F.

Type theory and realisability
Thursday March 16, 2017, 2PM, Salle 1007
Pierre-Marie Pédrot An Effectful Way to Eliminate Addiction to Dependence

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.