Groupe de travail

Équipe thématique Preuves et programmes


Jour, heure et lieu

Le mercredi à 14h, salle 1007


Contact(s)

Pour recevoir les annonces, s'abonner ici.


Prochaines séances


Théorie des types et réalisabilité
mercredi 14 mars 2018, 14h00, Salle 1007
Laura Fontanella (Institut de Mathématiques de Marseille) TBA


Séances précédentes


Théorie des types et réalisabilité
mercredi 14 février 2018, 14h00, 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/).

Théorie des types et réalisabilité
mercredi 31 janvier 2018, 14h00, 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.

Théorie des types et réalisabilité
mercredi 17 janvier 2018, 14h00, 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

Théorie des types et réalisabilité
mercredi 20 décembre 2017, 14h00, 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.

Théorie des types et réalisabilité
mercredi 06 décembre 2017, 14h00, 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.

Théorie des types et réalisabilité
mercredi 29 novembre 2017, 14h00, 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.

Théorie des types et réalisabilité
jeudi 16 mars 2017, 14h00, 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.