14h - 14h30 : D Kesner  (slides)

La théorie des substitutions explicites revisitée 

14h30 - 15h : P Baillot  (slides)

On Quasi-Interpretations, Blind Abstractions and Implicit Complexity

15h - 15h30 : K Nour  (slides)

La forte normalisation du lambda-calcul simplement typé avec des équations récursives sur les types

15h30 : Fin des journées


Jean François Monin : Normalisation dans une algèbre ACI par transformation de type

Dans l'étude de systèmes cryptographiques par des modèlessyntaxiques à la Dolev-Yao, on est amené à considérerdes algèbres de termes quotientés par une opérationassociative commutative et involutive : des attaques spectaculaires se basent en effet sur ces propriétés du ou exclusif bit à bit.
Nous tentons ici une approche où le calcul d'une forme normaled'un tel terme s'effectue en suivant non pas l'un des nombreux ordres bien fondés de la littérature, mais un retypage structuré de ce terme.


Daniel  de Carvalho : Construire de nouveaux modèles de la logique linéaire

Sous certaines conditions que l'on explicitera, la formule de Taylor-Ehrhard permet, à partir d'un modèle des réseaux différentiels, de construire des  modèles de la logique linéaire et du lambda-calcul. Cependant, les modèles ainsi obtenus ne rentrent pas nécessairement dans le cadre catégorique de  Benton, Bierman, Hyland et de Paiva. En particulier, on donnera un exemple très  simple d'un tel modèle. C'est pourquoi on commencera par donner un nouveau cadre catégorique aux sémantiques de la logique linéaire.

Matthieu Kaczmarek  : Théorème de la récursion et virus informatiques : expériences

 La correspondance entre le théorème de récursion de Kleene et la notion de  virus informatique a été souligné par de nombreux auteurs. Il est surprenant que  cette analogie n'est pas été approfondie en tant que modèle. Nous présenterons  plusieurs points communs entre la théorie de la récursion et la virologie informatique. Puis, nous illustrerons ces relations des exemples.  Enfin, nous montrerons comment   le théorème de récursion peut être utiliser en pratique.



Lutz Strassburger : Some Observations on the Proof Theory of MLL2

We present two new aspects of the proof theory of MLL2. First, we will give a novel proof system for in the framework of the calculus of structures. The main feature of the new system is the consequent  use of deep inference. Due to the new freedom of permuting inference rules, we are able to observe a decomposition theorem, which is not  visible in the sequent calculus. Second, we show a new notion of  proof nets which is inspired by the deep inference proof system. Nonetheless, the proof nets are independent from the deductive system. We have ``sequentialisation'' into the calculus of structures as well as into the sequent calculus. As expected, there is also a notion of cut elimination which is terminating and  confluent.


Richard Bonichon  :  Des tableaux pour la deduction modulo

La deduction modulo est un formalisme logique qui permet de meler etapes de deduction et de calcul dans le raisonnement. Ce cadre est particulierement adapte a la preuve automatique et a l'interaction avec l'etre humain. De plus, beaucoup de theories axiomatiques peuvent y etre exprimees sous forme de regles de calcul. Nous presentons une methode automatique de recherche de preuve  pour la deduction modulo fondee sur la methode des tableaux (TaMeD). Nous donnons les principaux resultats theoriques lies a cette methode, en particulier ceux concernant  l'elimination des coupures. Enfin, nous examinons comment implanter  TaMeD en utilisant le  demonstrateur automatique Zenon.

Olivier Laurent : Sémantique des jeux : du lambda-calcul à la logique classique du premier ordre

Si les modèles de jeux se sont développés pour prendre en compte de plus en plus de primitives de programmation (PCF, Idealized Algol,contrôle, non-déterminisme, probabilités, concurrence, ...), ils permettent également de fournir des modèles dénotationnels de différents systèmes logiques. Nous présenterons les modèles de jeux à la Hyland-Ong/Nickau pour le lambda-calcul simplement typé, et donc pour la logique intuitionniste minimale (qui datent de plus d'une décennie). Nous montrerons ensuite comment les étendre à la logique classique propositionnelle (lambda-mu calcul simplement typé) et enfin à toute la logique du premier ordre. La notion clef sous-jacente à ces différents modèles est celle de forme normale eta-longue pour les logiques considérées.


Ralph Matthes : Vérification d'un algorithme qui se sert d'une famille inductive de types 

Des familles inductives de types sont des types de données paramétrés non-uniformement: leurs constructeurs
 établissent des liens entre plusieurs membres de la famille. En anglais, on parle de "nested datatypes". 
Depuis la version 8.1 beta, le système Coq offre des outils natifs de programmation et de vérification des algorithmes qui
se servent de telles familles. Cependant, les invariants à prouver restent difficiles à trouver. Cela sera illustré à l'aide de l'exemple de la redécoration de configurations triangulaires de données, étudie dans l'article avec A. Abel et T. Uustalu dans TCS 333(1-2), pp. 3-66, 2005. L'implantation de l'algorithme dans Coq dépasse même les schémas proposés dans cet article. Donc, on se réjouit de la garantie de terminaison fournie par Coq et de la vérification formelle dans le même système.

Colin Riba : On the Stability by Union of Reducibility Candidates  

 We investigate some aspects of proof methods for the termination of (extensions of) the second-order lambda-calculus in presence of union  and existential types. We prove that Girard's reducibility candidates are stable by union iff they are exactly  the non-empty sets of terminating terms which are downward-closed  wrt a weak observational preorder.  We show that this is the case for the Curry-style second-order lambda-calculus. As a corollary, we obtain that reducibility candidates are exactly  the Tait's saturated sets that are stable by reduction. We then extend the proof to a system with product, co-product and positive so-recursive types.


Patrick Baillot : On Quasi-Interpretations, Blind Abstractions and Implicit Complexity 

Le Quasi-interprétations sont un outil introduit par Bonfante, Marion et Moyen pour garantir des bornes de complexité sur des programmes fonctionnels du premier ordre: couplées avec des ordres de terminaison elles fournissent en particulier une condition suffisante pour un programme pour être exécutable en temps polynomial ([MarionMoyen00]), appelée ici le P-critère. Nous étudions les propriétés des programmes satisfaisant le P-critère, de manière à analyser leur expressivité intensionnelle.
Etant donné un programme sur les listes binaires, nous définissons pour cela son  abstraction aveugle comme le programme non-déterministe obtenu en remplaçant les listes par leur longueur (entier unaire). Un programme est dit aveuglément polynomial si son abstraction aveugle termine en temps polynomial. Nous montrons que les programmes satisfaisant une variante du P-critère sont en fait non seulement exécutables en temps polynomial, mais aussi aveuglément polynomiaux. Nous proposons alors deux extensions du P-critère.



Julien Forest : Certification automatique de preuves de terminaison 


Les outils de demonstration automatique de la terminaison (CiME, Talp, Aprove, TTT, ...) sont devenus avec le temps de plus en plus
efficaces et puissants (cf. resultats de la derniere competition de terminaison http://www.lri.fr/~marche/termination-competition/2006/webform.cgi?command=trs).  Pour parvenir a ces resultats, ces outils, bien que fondes sur des resultats theoriques solides, sont devenus tres complexes (la taille du code de CiME est comparable celle du compilateur ocaml)  et les preuves generees sont de plus en plus difficiles a verifier "a la main". Le probleme de la validite des preuves generees est des lors pose. Nous developpons actuellement, dans le cadre du projet ANR A3PAT, une version de CiME fournissant une trace certifiable dans un assistant a la preuve (actuellement Coq) des preuves de terminaison obtenues. Nous presenterons notre demarche et notre prototype  capable de certifier des preuves impliquant des criteres complexes.



 Pierre-Yves Strub et Jean Pierre Jouannaud : Building Decision Procedures in the Calculus of Inductive Constructions 


It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within
deductions in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P' obtained from P thanks to possibly complex calculations. We investigated a new version of the calculus of inductive constructions which incorporates arbitrary decision procedures into deductions via the conversion rule of the calculus. Besides the novelty of the problem itself in the context of the calculus of inductive constructions, a major technical innovation of this work lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the  decision procedure together with the set of user hypotheses
available from the current context. Our main result shows that this extension of the calculus of constructions does not compromise its
main properties: confluency, strong normalization and decidability of proof-checking are all preserved. We will show in detail how a goal to be proved in the calculus of constructions is actually transformed into a goal in a decidable first-order theory. Based on this transformation, we are currently developping a new version of Coq implementing this calculus.

Damiano Mazza : Edifices: Boehm trees for the Symmetric Interaction Combinators

The symmetric interaction combinators are a variant of Lafont's interaction combinators. They are a graph-rewriting model of parallel deterministic computation. We define a notion analogous to that of head normal form in the lambda-calculus, and make a semantical study of the corresponding observational equivalence. We associate to each net a compact metric space, called edifice, with the property that two nets are observationally equivalent iff they have the same edifice. Edifices may therefore be compared to Boehm trees in infinite eta-normal form, or to Nakajima trees, but unlike these they give a precise topological account of phenomena like infinite eta-expansion.


Guillaume Burel : Réduction non-bornée de la longueur de preuves en déduction modulo

 En 1973, Parikh a démontré un théorème conjecturé par Gödel 37 ans  auparavant, qui dit qu'il est possible de trouver des formules de l'arithmétique qui sont toutes démontrables en arithmétique du première  ordre, mais dont la preuve la plus courte en arithmétique du second ordre est arbitrairement plus courte que n'importe quelle preuve au premier ordre. D'un autre côté, la résolution d'ordre supérieur peut être simulée pas à pas en utilisant une méthode de surréduction et de résolution du premier ordre basée sur la déduction modulo, dont le  paradigme est de séparer la déduction et le calcul pour rendre les preuves plus lisibles et plus courtes. Nous démontrons premièrement qu'il est possible de trouver des formules dont la plus petite preuve en déduction naturelle modulo est plus courte de façon non bornée par rapport à toute preuve en déduction naturelle
 pure. Deuxièmement, nous montrons qu'une preuve dans l'arithmétique  d'ordre $i+1$ peut être transformée linéairement en une preuve dans  l'arithmétique d'ordre $i$ modulo un système de réécriture fini,  terminant et confluent. Ceci nous permet d'affirmer que le gain sur la taille des preuve conjecturé par Gödel ne provient pas de la déduction,
mais peut être exprimé en tant que calcul, ce qui justifie l'utilisation  de la déduction modulo comme un outil du premier ordre efficace pour simuler l'ordre supérieur.

Paul Brauner et Clément Houtman : Surdéduction  

 Nous présentons la surdéduction, un moyen systématique d'internaliser une théorie dans un système d'inférences. Nous en présentons ensuite les principales propriétés : correction et complétude. Nous présentons ensuite un langage de termes associés aux preuves en surdéduction appliquée au calcul des séquents ainsi que la  terminaison de  l'élimination des coupures pour certaines classes de théories. Enfin nous présentons lemuridae, un assistant de preuve fondé sur ce formalisme.

Delia Kesner : La theorie des substitutions explicites revisitee 


Les calculs avec substitutions explicites ont émergé de manière très naturelle dans plusieurs domaines de l'informatique comme la programmation fonctionnelle et/ou logique, la théorie de la démonstration, la concurrence, les langages orientés objets, etc.  Des nombreux systèmes complexes avec substitutions explicites ont été développés ces dernières 15 années afin de capturer les bonnes propriétés opérationnelles du système original (avec méta-substitution) qu'ils visaient implémenter.
Nous  passerons  en revue  les  travaux dans  le  domaine  en pointant  les motivations et  défis qui ont guidés  le développent de  tous ces systèmes. Nous  utiliserons ensuite  une  technologie très  simple  pour établir  une théorie  générale  des   substitutions  explicites  pour  le  lambda-calcul vérifiant  des   bonnes  propriétés  comme   la  simulation  d'un   pas  de beta-réduction, la  confluence sur les  méta-termes, la préservation  de la normalisation forte,  la normalisation  forte pour les  termes typés  et la
composition forte.   Nous établirons aussi  un lien entre notre  théorie et les réseaux des démonstration de la logique linéaire.

Karim Nour et René David : La forte normalisation du lambda-calcul simplement typé avec des équations récursives sur les types

Je présente une preuve arithmétique de la forte normalisation du lambda-calcul simplement typé avec des équations récursives sur les types. La preuve utilisant les candidates de réductibilité est une simple extension de celle du lambda-calcul simplement typé sans équations mais cette preuve ne peut pas être formalisée dans l'arithmétique de Peano. La puissance du système nécessaire pour formaliser une telle preuve n'est pas connue. Notre preuve peut être formalisée dans l'arithmétique de Peano. Je présente aussi quelques applications et plusieurs questions ouvertes liées à ce sujet.