Preuves, Programmes et Systèmes

Groupe de travail Théorie des types et réalisabilité

Le groupe de travail se réunit en salle rose, verte ou orange au 5e étage, 23 avenue d'Italie (si extérieur, s'annoncer à l'accueil) [ liste de diffusion ]

Exposés à venir

Néant

Exposés passés

Vendredi 16 décembre, 14h, salle rose
Gyesik Lee
GMeta: A Generic Formal Metatheory Framework for First-Order Representations

GMeta is a generic framework for first-order representations of variable binding that provides once and for all many of the so-called infrastructure lemmas and definitions required in mechanization of formal metatheory. The framework employs datatype-generic programming and modular programming techniques to provide a universe representing a family of datatypes. Using this universe, several libraries providing generic infrastructure lemmas and definitions are implemented. These libraries are then used in case studies based on the POPLmark challenge, showing that dealing with challenging binding constructs, like the ones found in System System F with subtyping (F<:), is possible with GMeta. All of GMeta's generic infrastructure is implemented in Coq, ensuring the soundness of the generic infrastructure.

Mercredi 14 décembre, 14h, salle rose
Jamie Gabbay
Stone duality for first-order logic (a nominal approach)

I will present a brand new paper in which we prove a Stone duality between a nominal algebra axiomatisation of first-order logic (FOL-algebras), and a notion of topological space (forall-Stone spaces).

We are familiar with Boolean algebras being sets with conjunction and negation actions satisfying certain axioms. We are also familiar with the fact that powersets naturally have a Boolean algebra structure, given by interpreting conjunction as sets intersection and negation as sets complement.

Using nominal techniques we can axiomatise substitution and first-order logic, so we can try to extend the Stone duality theorem from Boolean algebras to FOL-algebras, and to some class of nominal topological spaces.

If we can answer this question, then we obtain a nominal representation of first-order logic without Tarski-style valuations. A variable populates the denotation directly as nominal atoms, and substitution acts on variables directly in that denotation. This is a very different view of variables in logical meaning than the one which the reader is most likely accustomed to.

The proofs contain a wealth of interesting structure and they give a sense in which variables really can directly inhabit denotations in logic and topology. The paper is online at my papers page. See also a precursor paper on Stone duality for the NEW quantifier.

Mercredi 30 novembre, 14h, salle rose
Yves Guiraud
Polygraphes et actions de monoïdes sur des catégories

Je présenterai un travail en commun avec Stéphane Gaussent et Philippe Malbos sur l'utilisation de méthodes de réécriture de dimension supérieure pour les actions de monoïdes sur des catégories.

L'objectif est de calculer, à partir d'une présentation d'un monoïde par générateurs et relations, une « base d'homotopie » engendrant toutes les relations entre les relations : cette donnée est exactement ce qui manque à une présentation pour obtenir une définition pratique d'action du monoïde sur des catégories.

Nous montrons comment des méthodes de réécriture (théorème de Squier, complétion de Knuth-Bendix), adaptées au cadre des polygraphes de Burroni, peuvent permettre de calculer cette base d'homotopie. Nous obtenons notamment ainsi une nouvelle preuve, algébrique et constructive, d'un résultat de Deligne sur les actions de groupes de tresses.

Mercredi 23 novembre, 14h, salle rose
Pierre-Marie Pédrot
Double-glueing and linear logic: models, polarization, games

Double-glueing is a categorical construction formalized by Hyland and Schalk, which is pervasive in models of linear logic. In a nutshell, it consists in refining a raw model through a realizability process, heavily relying on a notion of orthogonality between proofs and counter-proofs, akin to ludics.

I'll present this particular construct and underline the fact that most models of LL are a particular instance of double-glueing. Furthermore, it also provides a natural framework to understand polarization, by relaxing the double-orthogonal closure requirement of linear logic, and a better insight into the relationship between exponentials and polarization.

Finally, I'll try to convince the audience that such a realizability construction seems to be a legit way of integrating dependent types (and subtyping) into linear logic.

Mercredi 19 octobre, 14h, salle verte 2
Federico Aschieri
A new way of using Friedman's translation: Interactive Realizability

We present a classical realizability interpretation based on interactive learning. A realizer is an intelligent, self-correcting program, representing a proof/construction. This construction depends on some state, which is an approximation of an oracle for the Halting problem. The realizer interacts with the environment, which may provide a counter-proof, a counterexample invalidating the current construction of the realizer. But the realizer is always able to turn such a negative outcome into a positive information, which consists in some new piece of knowledge learned about an oracle for the Halting problem.

We then characterize this "interactive realizability" in terms of translation of classical into intuitionistic Arithmetic. It is known, for example, that Krivine's classical realizability is equivalent to Krivine-Streicher-Reus negative translation composed with Friedman's translation. On the other hand, interactive realizability is equivalent just to a special restricted Friedman translation. That is, one can see interactive realizability as a new use of Friedman's translation, that validates classical principles with out passing through negative translation, and yet is suitable for program extraction from classical proofs.

Mercredi 12 octobre, 14h, salle orange 1
Tim Griffin (Cambridge, in sabbatical in PPS)
A language of combinators for algebraic structures implemented in Coq

I'll describe ongoing work on a domain-specific language for implementing various algebraic structures (semirings, ordered semigroups, etc). Expressions in the language are made up of constants (representing simple algebras such as min-plus) and combinators that construct new structures from components (such as direct and lexicographic products).

The key feature of the language is that it has been designed so that a fixed class of important properties (such as distributivity, idempotence, commutativity, and so on) are automatically proved or refuted by the "type system" of the language. This allows a user to specify complex algebraic structures and obtain these proofs (or refutations) automatically. It is hoped that the language and its implementation will facilitate the rapid exploration of the algebraic design space.

We have implemented a prototype using the Coq theorem prover. All of the essential theorem proving (for the typing rules) is performed at "language design time." Users writing algebraic expressions at "specification time" do not run Coq directly. Rather, they run code that has been extracted automatically from the (constructive) proofs of our library of Coq theorems.

Much of the current implementation was done by my former PhD student, Vilius Naudziunas (now at Google), but I plan to continue this work during my sabbatical year at PPS.

Mercredi 14 septembre, 14h
Paul Downen
Building Up Multiple Control: From pure lambda-calculus to shift-upto

From type-directed partial evaluation to call-by-need application, multiple prompt control has many uses. However, there is still a need for a foundational account of control with multiple prompts.

In this talk, we will begin with the pure, call-by-value lambda-calculus and systematically derive languages with increased control. We will cover delimited control, where only a portion of the context is captured, and dynamic binding, where variables refer to the most recent binding rather than the nearest one. We will also review continuation- and environment-passing transforms and their use as a definition of semantics.

Mardi 28 juin, 15h (attention, jour et heure inhabituels)
Andreas Abel
Higher-Order Dynamic Pattern Unification for Dependent Types and Records

Higher-order unification is a central ingredient to type reconstruction in dependently typed languages. While undecidable in general, there exist decidable fragments such as Miller's pattern unification. In this talk, I recapitulate constraint-based unification modulo beta-eta and discuss several extensions as implemented in the dependently typed language Agda. Finally, I'll explain how to scale unification to strong Sigma-types, i.e., record types with eta laws.

Du mercredi 15 au vendredi 17 juin : workshop structural.

Mercredi 18 mai, 14h salle rose
Marco Gaboardi
Linear Dependent Types for Certified Resource Consumption
I present the ideas underlying the design of an interactive programming framework useful to ensure the reliability and correctness of programs with respect to their resource consumption. The key ingredient of this framework is a type system, dlPCF, mixing ideas coming from linear logic and dependent types. dlPCF is a joint work with Ugo Dal Lago that will be presented at LICS 2011. In this talk I introduce dlPCF and I show that it is sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of their evaluation. Additionally, dlPCF is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability. Finally, I will show a possible use of dlPCF combined with Krivine's Realizability in the setting of cost-preserving certified compilation.

Mercredi 11 mai, 14h, salle rose
Hugo Herbelin
An introduction to control calculi for classical logic
A posteriori, we can observe that more than 50 years were needed to get out of Gentzen's cut-elimination procedure for sequent calculus LK some intelligible constructive meanings to classical logic. I will try to give a survey of the main steps of the history of constructive classical logic, a domain that significantly sped up in the last 25 years after Felleisen et al designed the lambda-C calculus and Griffin revealed it provides with a direct-style extension of the proof-as-program correspondence from intuitionistic to classical logic. I will also try to give some basic criteria allowing to compare the different syntactic frameworks supporting classical logic.

Mercredi 4 mai, 14h, salle rose
Arnaud Spiwack
Adjunctions for the type-theoretist
Here is a common pattern in Computing Science conferences: the speaker drops, somewhere near his second slide, the word "adjunction". And then, suddenly, the room feels like 1940's London: almost no one is around anymore. If you're usually among the awkward part of the audience, returning to sleep or to the internet, this talk is meant for you. I will try and show how the notions of categories and adjunction can arise from a logical perspective. I aim at giving tools to the type theorist to develop an intuition about adjunction. This will suppose little prerequisite, namely familiarity with first order logics, a touch of Curry-Howard, and vague memories of algebra from your university classes.

Mardi 12 avril, 14h, salle rose (attention jour inhabituel)
Keiko Nakata
On trees that are finitely red (Proof Pearl with FAN and Bar Induction & finiteness)

Finiteness is a concept that seems as intuitive as it is fundamental in all of mathematics. At the same time finiteness is notoriously difficult to capture axiomatically.

In this talk, I look at several definitions of "finitely red" for binary red-and-black trees with infinite paths. Starting from all-black-trees, we gradually move to more reddish trees. Each definition comes with a tree-based view and a path-based view, which are not necessarily equivalent. Deriving tree-based views from path-based views are instances of FAN and Bar Induction. Our expedition arrives at a diagram of finitely redness which reads differently in constructive and classical settings: one edge uses LPO, therefore breaks constructively; one edge uses weak continuity, therefore breaks classically.

In the latter part of the talk, I examine a definition of binary sequences that are almost always zero. The definition comes out from the expedition and is new to us.

Joint work with Marc Bezem and Tarmo Uustalu.

Mercredi 23 février, salle rose à  14h
Georges Gonthier
Type Design Patterns for Computer Mathematics

Proof assistants such as the Coq system have traditionally been a laboratory for exotic type features such as dependent and computable types, and first-class type classes. Although these features have been introduced independently, it turns out they can be combined in novel and nontrivial ways to solve some of the more challenging problems posed by the formalization of advanced mathematics. Many of these patterns could also be useful for general programming.

Journées thématiques sur les modèles du calcul des constructions

Lundi 14 février, salle rose
11h: Alexandre Miquel, Classical realisability for the Calculus of Constructions (slides)
13h30: Andreas Abel, Normalisation-by-Evaluation for the Calculus of Constructions (slides)
15h: Bruno Barras, Formalizing a set-theoretical model of CIC in Coq/IZF (part I) (slides part I and II)

Mardi 15 février, salle rose
10h: Marc Lasson, Realizability and Parametricity in Pure Type systems (slides)
11h: Hugo Herbelin, What needs to be changed in CIC to make it compliant with Voevodsky's univalent model
11h30: Jeff Sarnat, Logical relations for sequent calculus with guarded (co)recursion
14h: Bruno Barras, Formalizing a set-theoretical model of CIC in Coq/IZF (part II)


Mercredi 26 janvier, salle orange 2
Guillaume Munch-Maccagnoni
From CPS to polarisation: a proof-theoretic decomposition of (delimited) CPS translations

The understanding of continuation-passing style (CPS) translations, an historical source of denotational semantics for programming languages, benefits from notions brought by linear logic, such as focalisation, polarities and the involutive negation. Here we aim to show how linear logic helps as well when continuations are delimited, i.e. return and can be composed, in the sense of Danvy and Filinski.

First we provide a polarised calculus with delimited control (first-class delimited continuations) which is, at the level of computation, a variant of Girard's polarised classical logic LC. It contains variants of delimited control calculi which spawned as answers to the question “what order of evaluation can we consider with delimited control?”. Thus our polarised calculus is one answer which is unifying to some degree.

Subsequently we decompose the calculus through polarised linear logic. The only difference with non-delimited continuations is the use of specific exponentials, that account for the specific semantics of the target of delimited CPS translation, as well as annotations of type-and-effect systems.

As a by-product, we obtain an explanation of CPS translations through a factoring, each step of which accounts for distinct phenomena of CPS translations. Although the factoring also holds for non-delimited CPS translations, it did not appear in its entirety before.

Mercredi 19 janvier, salle bleue 2
Bruno Woltzenlogel Paleo
Proof Compression: CIRes and Resolution Hypergraphs

The topic of proof compression involves challenging and under-investigated proof-theoretical problems as well as practical applications such as the efficient integration of theorem provers (Sat/SMT-solvers, automated provers, proof assistants...) via proof exchange.

In this talk, I will briefly show that defining the problem of proof compression in a precise, general and abstract way is not as straightforward as it might seem at first. Then I will proceed to describe two techniques that I have been developing recently.

The first technique, CIRes, consists of compressing sequent calculus proofs by introducing (atomic) cuts. CIRes works by extracting an unsatisfiable clause set from a cut-free proof P. By seeing resolution inferences as atomic cuts, any refutation of this clause set can then serve as a skeleton for a sequent calculus proof with atomic cuts. I will show that, in some cases, CIRes is capable of achieving an exponential compression in the size and length of proofs.

The second technique targets propositional resolution proofs, such as those output by Sat- and SMT-solvers. In order to more easily spot eliminable redundancies, I have developed a graphical way of looking at a resolution proof: its resolution hypergraph. Redundancies that appear far apart in the proof tend to appear close together in its hypergraph. Moreover, since resolution hypergraphs are invariant w.r.t. permutations of resolution inferences in their corresponding proofs, having the same hypergraph might be a good criterium for judging whether two resolution proofs are "essentially the same".

Mercredi 12 janvier, salle bleue 2
Olivier Danvy
A Synthetic Operational Account of Lazy Evaluation

Seen in Item 101B of HAKMEM (AI Memo, 1972), about continued fractions: We present the first operational account of lazy evaluation that connects theory and practice. Practice: the store-based implementation technique of using updateable thunks to account both for demand-driven computation and memoization of intermediate results, initiated by Landin and Wadsworth and prevalent today to implement lazy programming languages such as Haskell. And theory: the storeless operational semantics providing a completely syntactic support for demand-driven computation and memoization of intermediate results, initiated by Ariola, Felleisen, Maraist, Odersky and Wadler and prevalent today to reason equationally about lazy programs, on par with Barendregt et al.’s term graphs. Our operational account takes the form of two new calculi for lazy evaluation of lambda-terms and our synthesis takes the form of three bisimulations. The first calculus is a context-sensitive variant of Ariola et al.’s call-by-need lambda-calculus and makes “neededness” syntactically explicit. The second calculus uses updateable thunks and an algebraic store, where the storage structure induced by lazy evaluation is made explicit. Through the refocusing program-transformation technique, the first calculus gives rise to a storeless abstract machine and the second to a traditional store-based abstract machine implementing lazy evaluation. The machines are intensionally compatible with extensional reasoning about lazy programs and they are lock-step equivalent. Our result reveals a genuine computational unity of theory and practice.

Mercredi 5 janvier, salle rose
Matthias Puech
A logical framework for incremental type-checking

In this talk, I will present an ongoing work on a variant of the LF metalanguage, suitable for the core implementation of an incremental type-checker. Such a type-checker would allow eventually to provide in turn different "versions" of a typing derivation, of which only the differing sub-derivations are to be rechecked. This involves to finely track the dependencies between objects, usually hidden in LF's "flat" term syntax. This language features a rich notion of first-class reduction- and typing environments, and is stripped down from all its positional aspects. I will discuss some of the practical applications of such a type-checking discipline, as well as the currently open questions on its metatheory.

Mercredi 1er décembre, salle verte 2
Martin Hofmann
Relational semantics of effect-based program transformations

This is a status report on my ongoing collaboration with Nick Benton and Andrew Kennedy from Microsoft Research. Basically, our idea is to give a rigorous justification to effect-based program transformations such as

e1;e2 = e2;e1 provided that reads and writes of e1, e2 don't overlap

lambda x.let y=e1 in e2 = let y=e1 in lambda x.e2 provided that e1 is pure

etc

While these equivalences are reasonably obvious for straight-line programs with global store they become more intriguing when the participating program fragments contain free procedure variables that are merely specified by some contract such as "does not read", "is pure", ..., for then we must ascribe a precise semantic meaning to such a contract. Furthermore, effect descriptions like "is pure" "reads and writes do not overlap" might only hold "cum grano salis" in the sense that a program fragment deemed "pure" might very well modify parts of the store but only in some way that "doesn't matter", e.g. modify some internal data structures of the operating system for an extreme case or update some cached field for the sake of efficiency.

Our semantical justification should allow one in principle to make such arguments completely rigorous.

On the technical level, we will encounter admissible logical relations, regions, invariants, and also still open problem in basic domain theory.

Vendredi 26 novembre, salle orange 1, à 9h30
Randy Pollack
A Canonical Locally Named Representation of Binding
Joint work with Masahiko Sato

Binding is fundamental in mathematics and computer science. We must be able to formally represent and reason about binding to carry out a program of mechanising metatheory in computer science. One broad approach uses distinct syntactic classes of "parameters" (used for free or globally bound variables) vs "local variables" (used for bound variables). This general idea, which we call local representation, goes back (informally) to Frege.

In 1992 McKinna and Pollack formalised a local representation using distinct classes of names for parameters and variables. This representation is not canonical (terms have more than one representation) but much metatheory of Pure Type Systems was formalised without the need to reason about (or even define) alpha-equivalence.

In the present work we give a refinement of McKinna–Pollack representation that is canonical. The central idea that makes this possible is due to Sato. The work is formalised in Nominal Isabelle.

References: Journal of Symbolic Computation 45 (2010) pp. 598-616, Journal of Automated reasoning (to appear)

Mercredi 24 novembre, salle rose
Olivier Danvy
CPS for ever

A quoi servent les continuations? De quoi sont-elles faites? Comment sont-elles représentées? Et comment s'en sert-on? Le but de cet exposé de travail est de répondre à ces questions classiques, avec les résultats clés du domaine, des exemples simples, et des cas de situation motivant d'abord les continuations non-délimitées et ensuite les continuations délimitées.

Mercredi 3 novembre
Stefan Hetzl
Some remarks on the (non-)confluence of classical logic

A Curry-Howard correspondence for an intuitionistic natural deduction system can often be obtained in a canonical way as a confluent and terminating term calculus. In sequent calculus formulations of classical logic the general set of reduction rules (i.e. without fixing a particular reduction strategy) is not confluent. Fixing a suitable strategy one obtains a confluent and strongly normalising reduction corresponding for example to call-by-name or call-by-value. However, the general reduction without strategy is hardly investigated.

This talk will be about the question which normal forms can be obtained from the general reduction. The work is carried out in first-order logic using Herbrand-Disjunctions as convenient mechanism for comparing cut-free proofs. A first result will show that the number of different normal forms is extremely large: it can grow as fast as the size of the normal forms (non-elementary). A second result will show that despite this, all of these normal forms do share certain structural properties which can be characterised by a regular tree grammer. Finally, I will speak about partial results and work in progress towards obtaining stronger results in the spirit of the second one.

Jeudi 21 octobre, 14h, salle verte
Alexandre Miquel
Une analyse calculatoire de la transformation de preuve par forcing

Le forcing est une technique inventée par Cohen pour démontrer la cohérence et/ou l'indépendance de certains axiomes vis à vis de la théorie des ensembles. Du point de vue de la théorie de la démonstration, le forcing repose sur une traduction des formules et des preuves paramétrée par un ensemble ordonné quelconque: l'ensemble des "conditions de forcing". Récemment, Krivine a proposé une méthode permettant de combiner le forcing avec la théorie de la réalisabilité classique, et a montré que la traduction des preuves par forcing correspond (au niveau des termes de preuves à la Curry) à une transformation de programme étonamment compréhensible.

Suite aux travaux de Krivine, je montrerai comment reformuler le forcing en arithmétique d'ordre supérieur, en me plaçant dans une extension adéquate du système F-omega (classique) avec termes de preuves à la Curry. Je présenterai la traduction des formules et la transformation de preuve-programme sous-jacente. Enfin, j'analyserai le comportement calculatoire des programmes traduits, et en déduirai une extension de la machine de Krivine avec environnements explicites - la KFAM - conçue pour traiter directement les preuves par forcing sans passer par la transformation de programme. Je concluerai sur les liens que cette étude fait apparaître entre la méthode de forcing et certains principes à la base des systèmes d'exploitation, ainsi que sur les perspectives en logique.

English abstract

Mercredi 22 septembre, 14h, salle rose
Andrej Bauer
Programming with algebraic effects
(contents of the talk)

Eugenio Moggi's observation that computational effects are monads has been very influential and is known to every Haskell programmer. Gordon Plotkin and John Power promoted the idea that computational effects are not "just" monads, but also algebraic theories that refine monads with operations and equations. Gordon Plotkin and Matija Pretnar recently explained the nature of handlers for computational effects in terms of algebra homomorphisms.

Such a well-rounded theoretical development deserves to be taken to practice. Thus, in an effort to make algebraic theories and algebra homomorphisms known to every programmer (of a certain kind), we have developed a simple programming language Eff based on the idea that computational effects are described by operations and handlers. Eff allows the programmer to define new computational effects and handle existing ones with great flexibility. Importantly, in contrast to Haskell monads, effects in Eff can be mixed seamlessly. It turns out that in Eff we also get delimited continuations for free, which is remarkable since continuations are the leading example of a computational effect that cannot be described by an algebraic theory.

This is joint work with Matija Pretnar from University of Ljubljana.

Jeudi 9 septembre, salle 6A92, 175 rue du Chevaleret
Carsten Schürmann
Tutorial on Twelf
10h-11h15 présentation de Twelf
11h30-12h45 session d'introduction sur machine (apporter son portable)
14h-17h session sur machine (pause incluse)

Mercredi 8 septembre, 14h, salle orange
Carsten Schürmann
Linear Contextual Modal Type Theory

When one develops, implements, and studies type theories based on substructural logics, for example, in the context of theorem proving, logic programming, and formal reasoning, one is immediately confronted with questions how to deal with logic variables.

In this talk, I define a linear contextual modal type theory that gives a mathematical account of the nature of logic variables. Our type theory is an conservative extension of intuitionistic contextual modal type theory proposed by Nanevski, Pfenning, and Pientka. It is sound, a result that was mechanically verified in the Twelf proof assistant, and it is extremely useful: it is the key to understanding linear explicit substitution calculi and linear pattern unification.

Exposés de l'année universitaire 2009-2010

Mercredi 14 juin, 14h, salle rose
Thomas Seiller
Graphes d'interaction

Je présenterai une sémantique localisée du fragment multiplicatif de la logique linéaire (MLL) où les preuves sont représentées par des graphes. Cette sémantique, inspirée des derniers travaux de J.-Y. Girard, se révèle être une version combinatoire de la géométrie de l'interaction dans le facteur hyperfini. Elle permet en particulier de mettre en rapport ces récents développements et les réseaux de preuves, les sémantiques de jeu ou la ludique.

Mercredi 19 mai, 14h, salle orange
Alois Brunel
Church => Scott = PTIME: an application of resource sensitive realizability

We introduce DIAL_lin, a dual variant of intuitionistic linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. Recasting an older result of Leivant and Marion, we give a characterization of the complexity class PTIME as the functions representable by a lambda-term of type 'Church' => 'Scott', where 'Church' is the type of usual Church binary words and 'Scott' the type of Scott words (a purely linear representation of words).

We will focus on the technique used to prove the soundess part of this result. It is a variant of the Dal Lago & Hofmann's realizability framework, which both gives meaning to the logic and allows us to bound the runtime of any typable lambda-term. We will discuss the possible extensions and simplification of this construction.

Mercredi 21 avril 2010, 14h, salle rose
Jeffrey Sarnat
Syntactically Finitary Account of Logical Relations (or: Do You Really Trust Your Proofs?)

Logical relations are a class of mathematical structures that are widely used to prove a variety of theorems about both programming languages and logics. Examples include normalization/cut-elimination (e.g. Girard's reducibility candidates, Luo's saturated sets), parametricity and contextual equivalence. Proofs by logical relations are popular both because they scale well to new theories, and because they provide a somewhat uniform method for proving what might otherwise be incredibly difficult theorems. In particular, they are most popular for proving foundational properties that are closely related to the notion of logical consistency, and in some cases (e.g. the normalization for System F) some variation on a proof by logical relations is nearly the only game in town; we will see why this is not entirely a coincidence.

Gödel's second incompleteness theorem more-or-less states that any non-trivial logic is incapable of proving its own consistency; in other words, in order to prove some consistency result R, you must, at some level, make proof-theoretic assumptions R' which are at least as strong as assuming R outright. This dealt a harsh blow to Hilbert's program, whose aim was to demonstrate the consistency of all mathematical reasoning via minimalistic, "finitary" reasoning, which turned out to be impossible. However, if we view consistency proofs as finitary reductions between proof-theoretic assumptions (analogous to how Karp reductions are polynomial-time reductions from the complexity of one decision procedure to another), then such proofs become interesting for both philosophical and pragmatic reasons. Here, we give such an account of proofs by logical relations and, time permitting, how they can be tied into the branch of proof theory known as "ordinal analysis."

Mercredi 14 avril 2010, 14h, salle rose
Jeremy Avigad (professor of Philosophy and Mathematical Sciences, Carnegie Mellon University; currently visiting the INRIA - MSR Joint Research Centre in Orsay)
Forcing and Hilbert's program

Although much of Hilbert's rhetoric in the 1920's was focused on the problem of establishing the consistency of infinitary classical methods, the program can be more broadly viewed as an attempt to reconcile modern methods with more explicitly computational approaches that dominated mathematics through the nineteenth century.

After Gödel's discovery of the incompleteness theorems, proof theory turned to the general reductive program of justify classical theories relative to constructive ones. Forcing methods have proved to be a remarkably effective tool in this regard, providing syntactic ways of adding "ideal" objects in a conservative way. In this talk, I will discuss a number of examples, and explain how forcing methods can be used to provide constructive interpretions of weak König's lemma (a compactness principle), Ramsey's theorem for pairs, skolem functions, model-theoretic arguments, and more.

Mercredi 7 avril 2010
Après-midi thématique sur les systèmes de types purs

de 14h à 15h15
Denis Cousineau
Sound and complete candidates for λΠ modulo

Proof normalization is a fundamental property that ensures witness and disjunction properties for constructive proofs, completeness of certain methods of automated deduction, etc... In 1971, following the work of Tait, Girard developed a method, called reducibility candidates, for building proofs of strong normalization, giving, by the universal aspect of its method, a sound criterion for proof normalization in various logical frameworks. But this criterion is not known to be complete, there could exists normalizing theories for which one cannot build such a set of reducibility candidates.

In this talk, we present how to refine this notion of reducibility candidates in order to provide a sound and complete criterion for proof normalization. This criterion is defined for the λΠ-calculus modulo, a logical framework with dependent types in which theories such as functional Pure Type Systems can be expressed within a set of rewrite rules.

de 16h à 17h15
Vincent Siles
A unified view of PTS's conversion

Pure Type Systems (or PTS) are a generic framework which allow to deal with several systems (Simply Typed Lambda Calculs, System F, Calculus of Constructions,...) all at once. Those systems mostly rely on an untyped notion of equality called conversion, which is based on program evaluation. To prove some theoretical properties of those systems, like their consistency in presence of external axioms, we may need to type the process of evaluation, leading to the notion of PTS with "judgmental equality". However the theory behind this typed equality is strangely difficult to establish: the proofs of Confluence, Subject Reduction or Injectivity of Products are all linked together in a circular dependency. A few years ago, Robin Adams managed to prove that for the particular subclass of functional PTS, both visions of the conversion were equivalent. His proof uses a intermediate system which mixes ideas from confluency and typing, called Type Parallel One Step Reduction (TPOSR). But in the end, the question whether this is true for all PTS remains open. After a review of the already known results about PTS, I'll present a proof that this equivalence holds for an alternative class of PTS called "semi-full", based on Adams's TPOSR and Jutting's study of types in general PTS. Then, I'll give some hints on proving such an equality for systems involving sub-typing.

Mercredi 24 mars 2010, 14h, salle rose
Stéphane Glondu
Certifying Coq's extraction: the internal extraction approach
The extraction in Coq consists in removing some parts of Coq terms that are irrelevant for computation and turn the remaining parts into programs in a practical programming language such as (purely functional) OCaml. Its principle and several aspects of its current implementation have been described and studied by Pierre Letouzey in his PhD thesis. There is still a gap between the paper proofs and the implementation, though.

In this talk, I will remind the principle of Coq's extraction, a definition of correctness based on operational semantics, and how it can be stated and proved inside Coq. I will present the "internal extraction" approach, where the extraction function itself is not proved, but generates correction proofs instead. In this approach, the target language is formalized in Coq, but the source language doesn't need to be and its semantics is used implicitly.

Mercredi 3 mars 2010, 14h, salle rose
Danko Ilik
Constructive Completeness Theorems and Delimited Control

Motivated by facilitating reasoning about meta-theory inside the Coq proof assistant, we revisit constructive proofs of completeness theorems.

In the first part of the talk, we discuss Krivine's constructive proof of completeness of classical logic and its computational contents. Then we present a class of Kripke-style models for which completeness can be shown via a normalisation-by-evaluation proof, and we compare its computational behaviour to the one of Krivine's proof.

In the second part, we revisit constructive completeness of intuitionistic logic (with disjunction and the existential) w.r.t. Kripke models. We discuss Danvy's Ocaml program for normalisation-by-evaluation of simply-typed lambda calculus with sums, and delimited control operators therein used. From his program, we extract a notion of model (which has the same shape as the notion presented in part 1 of the talk) that is sound and complete for full intuitionistic predicate logic. Finally, we present the cube of Herbelin and discuss some potential gains of adding delimited control operators to an intuitionistic or classical proof system.

Mercredi 24 février 2010, 14h, salle rose
Arnaud Spiwack
Mathematics without Unique Choice

I will present in this talk the principles of choice and unique choice, and how they are usually articulated around constructive mathematics. From this starting point, I will describe why the unique choice, which is traditionally valid, is a hindrance in the project of writing computationally efficient mathematics. Fortunately, the principle of unique choice is not provable in Coq, due to the (weak) irrelevance of the sort of propositions. The separation of the sort Prop from the rest of the logic was motivated by program extraction, which is, of course, related to the problem of efficient mathematics. In a sense, we will seek to give some mathematical substance to the pragmatics behind Prop. I will discuss the mathematical consequences of dropping the unique choice (a lot of things break, some seriously. That's the cost of efficiency).

Mercredi 10 février 2010
Après-midi thématique sur la sémantique des langages de bas niveau

de 14h à 15h30
Derek Dreyer (Max Plank Institute for Software Systems MPI-SWS)
The Art of the State in Logical Relations
(joint work with Amal Ahmed, Andreas Rossberg, Georg Neis, and Lars Birkedal)

Logical relations are a powerful method for reasoning about observational equivalence of higher-order programs. Although they were originally developed for pure languages like System F, they have in the last decade been generalized successfully to handle languages with semantically tricky features, such as general recursive types and higher-order mutable state.

In this talk, I will present an overview of some of our recent work on developing "step-indexed" Kripke logical relations for ML-like languages. One of the central ideas of our work is that, when reasoning about local state, establishing *invariants* on the local state is not enough; rather, one must be able to establish properties about local state that *change* (in a controlled way) over time. Thus, the possible worlds that we use to index our Kripke relations are essentially state transition systems (STS's), with each state corresponding potentially to a different relation on heaps. In the first part of the talk, I will motivate and sketch the details of our original logical relations model (POPL'09), using a representative example of a "generative ADT" (i.e. an ADT that uses local state to dynamically generate fresh inhabitants of the abstract type).

In the second part of the talk, I will present some brand new work in which, inspired by game semantics, we show how to generalize our POPL'09 model in several orthogonal directions. First, we can account for the concept of "well-bracketed" state change (familiar from game semantics) by enhancing our STS's with (1) "private" transitions and (2) "inconsistent" (or "reject") states. Second, we can account for the presence of control operators (call/cc) using biorthogonality (TT-closure). Third, we can account for the difference between first- and higher-order state by observing that the former enables one to sometimes make *illegal* state transitions while the latter does not. These extensions can be combined in quite interesting ways – for instance, we can prove the subtle "callback with lock" equivalence of Banerjee and Naumann in a language with first-order state and call/cc, as well as in a language with higher-order state but no call/cc. (In the presence of both higher-order state and call/cc, the equivalence doesn't hold.) Furthermore, due to our use of biorthogonality, it is straightforward to show that our logical relations are not only sound but also complete w.r.t. observational equivalence.

de 15h30 à 16h
Pause café

de 16h à 17h30
Sandrine Blazy (IRISA)
Mechanized semantics for the Clight language

In this talk, I will present the formal semantics of a large subset of the C language called Clight. Clight is the source language of the CompCert compiler. This compiler is formally verified using the Coq proof assistant. It guarantees that each compiled program behaves as prescribed by the semantics of its source program. The formal semantics of Clight is a small-step, continuation-based semantics that enables nontrivial reasoning about program transformations. This semantics is also equipped with traces of input/output events that observe both terminating and diverging executions, thus leading to stronger properties of observational equivalences. In addition, I will describe the integration of the Clight formal semantics in the CompCert compiler and several ways by which the semantics was validated.

Mercredi 3 février 2010, 14h, salle rose
Tristan Crolard (LACL – Université Paris-Est) : Dependent Type Systems for delimited control operators
(joint work with Emmanuel Polonowski) (pdf)

Relying on the formulae-as-types paradigm for classical logic, we define a dependent type system for an imperative language with higher-order procedural variables and non-local jumps. As a by- product, we obtain a non-dependent type system which is more permissive than what is usually found in statically typed imperative languages. We also show that this framework is expressive enough to encode imperative versions of the delimited continuations operators shift and reset, and we derive a program logic for these operators.

Mercredi 20 janvier 2009, 14h, salle rose
Pierre Letouzey : Les évolutions récentes des bibliothèques modulaires de Coq

FSets, FMaps, Numbers, OrderedType, etc: ces structures modulaires peuplent maintenant la bibliothèque standard de Coq depuis un bon moment. Dans cet exposé, je compte montrer que la situation de ces aspects de la bibliothèque standard est très loin d'être figée. De façon générale, on bénéficie maintenant en plein des travaux récents d'Elie Soubiran, à la fois sur la théorie des modules, et sur leur implémentation concrète (p.ex. ajout d'un "Include"). De mon coté, je présenterai les améliorations pratiques de ces bibliothèques, en particulier grâce à quelques petites modifications additionnelles du système de modules réalisées en collaboration avec Elie: application d'un foncteur au contexte local, chaînage d'"Include", etc etc. Ces modifications fournissent désormais un niveau de flexibilité et de modularité encore jamais atteint en Coq.

Mercredi 13 janvier 2010, 14h, salle rose
Matthieu Sozeau : Equations: a dependent pattern-matching compiler

We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functions, automatically find their realization in the core type theory and generate proofs to ease reasoning on them.

The basic functionality is the ability to define a function by a set of equations with patterns on the left-hand side and programs on the right-hand side, in a similar fashion to Haskell function definitions. The system also supports with-clauses (as in Epigram or Agda) that can be used to add patterns on the left-hand side for further refinement. Both "syntactic" structural recursion and "semantic" well-founded recursion schemes are available in definitions, the later being generalized enough to cope with general inductive families efficiently.

The system provides proofs of the equations that can be used as rewrite rules to reason on calls to the function. It also automatically generates the inductive graph of the function and a proof that the function respects it, giving a useful elimination principle for it. It gives a complete package to define and reason on functions in the proof assistant, substantially reducing the boilerplate code and proofs one usually has to write, also hiding the intricacies related to the use of dependent types.

Mercredi 6 janvier 2010, 14h, salle rose
Noam Zeilberger : Classical polarity and delimited continuations

Fact: classical polarized logic is the logic of continuation-passing style, in the sense that different logical fragments capture different fragments of CPS. This fact naturally suggests two questions:

1. What does classical polarity have to do with the "polarity-like" phenomena of various intuitionistic systems? In particular, type theories such as Levy's Call-By-Push-Value and Watkins et al's Concurrent Logical Framework seem to maintain polarity distinctions, but in an oddly restricted way (e.g., with no "par" connective). And they have no special connection to CPS.

2. What does classical polarity have to do with *delimited* continuation-passing? This is an important question, because empirical and theoretical evidence suggests that delimited continuations are in fact more suitable as a general framework for reasoning about effects and evaluation order.

In the talk I will try to answer these questions. In short, the answer is that "answers are positive".

Mercredi 9 décembre 2009: pas de réunion du GT (habilitation à diriger des recherches de Alexandre Miquel à 10h; à noter aussi l'habilitation de Antonio Bucciarelli le jeudi 10 décembre à 16h30)

Mercredi 2 décembre 2009 à partir de 14h en salle orange
Après-midi thématique sur la sémantique des langages de bas niveau

de 14h à 15h30
Chung-Kil Hur (PPS)
Observational equivalence on low-level programs and compositional compiler correctness
(Joint work with Nick Benton)

Giving a good notion of observational equivalence on low-level programs is particularly difficult due to the presence of non-functional operations such as those examining instructions of function closures. In the talk, (1) I discuss this difficulty by giving instructive examples in the untyped lambda calculus extended with the operation that tests alpha-equality of two terms; (2) give a notion of equivalence on those lambda terms by means of logical relation equipped with step-indexing and biorthogonality; (3) explain how to use this relation to give a compositional notion of correctness of compilers and hand-optimizations; (4) and finally discuss limitations of step-indexing and future work. These results have been fully formalized using the Coq proof assistant.

de 15h30 à 16h
Pause café

de 16h à 17h30
François Pottier (Gallium, INRIA Rocquencourt)
Hidden state and the anti-frame rule.

Modular reasoning about heap-manipulating programs relies on two important features.

One is the ability to make part of the store temporarily invisible – more precisely, invisible within a lexical scope – so as to be able to invoke a piece of code that does not know about this part of the store. This mechanism, known as local reasoning, is formalized, in separation logic and in type-and-capability systems, in terms of frame rules.

The other is the ability to make part of the store invisible forever – more precisely, invisible outside of a lexical scope – so that a piece of effectful code, packaged together with its state, is able to masquerade as effect-free code, and can be invoked by a client that does not know about this part of the store. This mechanism is known as hidden state.

The idea of hidden state goes back to Hoare (1972). However, its formulation in the setting of a program logic for a modern programming language, with higher-order functions and dynamic memory allocation, is challenging. There have been attempts to explain hidden state in terms of local reasoning, that is, in terms of (higher-order) frame rules. In this talk, I argue that this approach to hidden state imposes a continuation-passing style, which is impractical. Instead, I offer a direct explanation of hidden state, in the form of a so-called (higher-order) anti-frame rule.

I present this rule in the setting of a type-and-capability system for an ML-like programming language. I will discuss several applications of the rule, with example code.

Mercredi 25 novembre 2009, 14h, salle rose
Alexis Saurin: Une hiérarchie de calculs pour le contrôle délimité en appel par nom

Je présenterai une hiérarchie de calculs étendant naturellement le Λμ-calcul: les Λⁱ-calculs, qui constituent une version en appel par nom de la hiérarchie CPS de Danvy et Filinksi. Cette hiérarchie est motivée par deux éléments caractéristiques du Λμ-calcul comparé à son grand-frère, le λμ-calcul de Parigot:

• Λμ est une version en appel par nom des calculs avec contrôle délimité comme l'ont mis en évidence Herbelin et Ghilezan;
• Λμ est à la base d'un calcul de streams, la μ-abstraction pouvant être vue comme une abstraction sur une famille infinie de variables, on peut ainsi le voir comme un λ-calcul transfinitaire.

On obtient ainsi une famille de calculs possédant de très bonnes propriétés, pour laquelle on peut établir précisément la correspondance avec la hiérarchie CPS.

Mercredi 18 novembre 2009, 14h, salle rose
Hugo Herbelin: On the logical content of control delimiters

Danvy-Filinski's reset and Felleisen's prompt are operations that delimit the scope of the continuation caught by a control operator. In the continuation-passing-style semantics, their role is to reset the current continuation with the identity continuation and it turns out that this is similar to what happens in Friedman's A-translation.

A-translation is a tool to prove the intuitionistic admissibility of Markov's principle. We will then show that the extension of intuitionistic logic with delimiters allows to reason with A-translation in direct style and to prove Markov's principle (i.e. ¬¬∃x.A(x) → ∃x.A(x) for A decidable).

More generally, we will show that adding delimiters to classical logic provides with a way to internally extract the intuitionistic content of classical proofs (if any).

Jeudi 12 novembre 2009, 13h30, salle rose
Andreas Abel: Remarks on Typed Equality for the Calculus of Constructions

Martin-Löf Type Theory is usually presented with a typed equality judgement,

Γ ⊢ t = t' : A

expression that in context Γ, the terms t and t' are of type A and βη-equal. Typed equality has some advantages over untyped equality: The soundness theorem for models is easier to establish, and equality can be easily extended by axioms that need typing, like βη for the unit type or proof irrelevance. On the downside, implementations of equality checks use untyped reduction or evaluation, meaning that a subject reduction theorem has to established for untyped reduction. Subject reduction in turn depends on the infamous "injectivity of Π" property, which is trivial for confluent untyped equality, but notoriously hard for typed equality. The implementation of type checking depends crucially on the injectivity of Π, even if one assumed subject reduction.

In this talk, I will first present the state of the art of typed equality for Martin-Löf Type Theory: How one constructs a PER model which yields a typed normalization algorithm (normalization by evaluation) and injectiviy of Π. How one obtains a sound and complete type checker from these results. Then I will sketch how to transfer these results to the Calculus of Constructions.

Mercredi 4 novembre 2009, 14h, salle orange 2
Pierre-Louis Curien: La dualité du calcul à travers les lunettes de la focalisation

Nous adaptons le kit syntaxique de Curien-Herbelin afin de donner un compte-rendu syntaxique précis des preuves focalisées (en calcul des séquents) de la logique linéaire. L'exposé analyse divers choix syntaxiques, que l'on regroupe de manière générique (en suivant Munch) sous le nom de "système L".

L'exposé comprend cinq parties ....

Mercredi 21 octobre 2009, 11h, salle orange 1
Noam Zeilberger: Towards a Proof-Theoretic Semantics of Programming

In this talk, I will present some ideas and results from my thesis [1] aimed at narrowing the gap between the theory and practice of propositions-as-types. In particular, I will examine the proof-theoretic notion of polarity, explain its connection to the old idea (of Gentzen, Prawitz, Dummett, and others) of a proof-theoretic "justification" of the logical connectives, and describe how to extend polarized logic into a *polarized type theory* capable of analyzing the critical concepts of evaluation order and pattern-matching in modern functional languages. In addition, I will explain the role of "focusing" ( la Andreoli) in polarized type theory, and a connection between focusing and infinitary proof theory that enables one to give a uniform account of both untyped and intrinsically-typed computation (with cut-elimination and eta-expansion defined in a connective-generic way). And finally I will explain how this framework can be used to study *extrinsic* types (such as intersection and union types), and discuss some interesting partial results relating proof-theoretic and model-theoretic notions of subtyping.
[1]"The Logical Basis of Evaluation Order and Pattern-Matching", available at http://reports-archive.adm.cs.cmu.edu/anon/2009/abstracts/09-122.html