Seminars of the Protheo team - Year 2005-2006

2006

July 21 at 11:00
CoLoR : a Coq Library on Rewriting and termination, Frédéric Blanqui

Coq is a tool for certifying proofs. The aim of the CoLoR library is to provide the necessary formal basis for certifying termination proofs of rewrite systems. I will present the current state of the library.

July 21 at 11:30
Génération de preuves Coq pour la terminaison de systèmes de réécriture, Loredana Tec

Je vais faire une brève présentation sur mon travail de stage. Il s'agit de génération automatique de preuves Coq pour la terminaison de systèmes de réécriture, utilisant les formalisations dans CoLoR de RPO et des interpretations polynomiales.

June 22 at 16:00
Un calcul des séquents extensibles, Paul Brauner

Nous présentons un calcul des séquents inspiré de la déduction surnaturelle qui encode les axiomes d'une théorie exprimée par un système de réécriture sous la forme de nouvelles règles de déduction. Après en avoir étudié les principales propriétés et variantes, nous présentons un prototype d'assistant a la demonstration fondé sur ce système de déduction.

June 22 at 15:00
Formal Islands, Emilie Balland

Motivated by the proliferation and usefulness of Domain Specific Languages as well as the demand in enriching well established languages by high level capabilities like pattern matching or strategic rewriting, we introduce the Formal Islands framework. The main idea consists to integrate, in existing programs, formally defined parts called Islands, on which proofs and tests can be meaningfully developed. Then, Formal Islands could be safely dissolved into their hosting language to be transparently integrated in the existing user environment. The paper presents this generic framework and shows that the properties valid on the formal islands are also valid on the corresponding dissolved host codes. Formal Islands can be used as a general methodology to develop new DSL and we show that language extensions like sqlj ---embedding sql capabilities in Java ---, or Tom ---a Java language extension allowing for pattern matching and rewriting---are indeed Islands and they can therefore be used for formal software developments.

June 22 at 14:00
Le Calcul des Constructions Congruentes, Pierre-Yves Strub

Le Calcul des Constructions Congruentes (CCC) est une extension du Calcul des Constructions dans laquelle la règle de conversion fait usage de procédures de décision au premier ordre. En partant d'exemples, je présenterai comment faire une telle intégration, puis donnerai une description détaillée du nouveau calcul et discuterai des pistes possibles pour une preuve de cohérence de ce dernier.

June 8 at 14:00
Prouver la terminaison presque sûre positive, Florent Garnier

Je présenterai dans cet exposé, les dernières avancées qu'Olivier et moi avons apporté dans l'étude des propriétés des systèmes de réécriture probabiliste. Après un bref rappel de ce que sont les systèmes de réécriture probabiliste et les stratégies dans ces systèmes, j'énoncerai la notion de terminaison presque sûre positive sous stratégies, puis je présenterai quelques méthodes permettant de prouver cette propriété et enfin je conclurai par quelques exemples.

June 2 at 10:00
A rho-calculus extension for molecular complexes, Oana-Maria Andrei

I will present our latest work on defining a language for molecular complexes and the interactions between them, with the aim of providing a formal model for reasoning and predicting the behavior of the biochemical systems. This language is in fact a particular extension of the rewriting calculus.

May 22 at 11:00
Constraint based termination, Colin Riba

In a previous work, F. Blanqui extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and by allowing explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can prove the termination of more functions. We first give a general type-checking algorithm based on constraint solving, where the constraint domain is abstracted away. Then, we give a termination criterion based on type-checking with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.

April 18 at 10:30
Optimisation de programmes par reconnaissance de templates, Christophe Alias

La plupart des optimisations appliquent des transformations locales bas-niveau, sans se soucier du calcul exprimé par le programme. Bien que ces optimisations produisent des résultats satisfaisants, elles ne se substituent pas à un bon algorithme, et amènent bien souvent le programmeur à utiliser des bibliothèques optimisées. Pour le moment, les bibliothèques optimisées doivent être appelées à la main. Apprendre et utiliser une nouvelle bibliothèque est malheureusement très fastidieux, et il est surprenant de voir le peu d'aide apporté par le compilateur. Une solution naturelle serait de chercher les occurrences des fonctions d'une bibliothèque dans le programme, et de les remplacer par l'appel correspondant.

Mots-clés :

  • Modèle polyédrique
  • Equivalence sémantique
  • Matching du second ordre

April 10 at 14:00
Questions juridiques liées à la pérénisation de la société de l'information, Isabelle de Lamberterie

  1. Les finalités de la conservation: preuve mais aussi conservation du patrimoine culturel.
  2. Que conserve-t-on? dans quelles conditions?: le dépôt légal du web, les archives numériques, la fiabilité des preuves informatiques.

April 6 at 11:00
Polygraphes, réécriture et logique, Yves Guiraud

La structure de polygraphe fournit un langage algébrique et graphique unificateur pour de nombreux objets algébriques, incluant naturellement les notions de calcul et de démonstration. Nous verrons ce que sont ces polygraphes, ainsi que quelques propriétés, au travers deux exemples : les systèmes de réécriture de termes et les démonstrations du calcul propositionnel.

March 23 at 14:00
Distributive rho-calculus, Clément Houtmann

The rewriting calculus has been originally designed and used for expressing the semantics of rule based as well as object oriented paradigms. We have previously shown that convergent term rewriting systems and classic strategies can be encoded naturally in the calculus.
In this paper, we go a step further and we propose an extended version of the calculus that allows one to encode unrestricted term rewriting systems. This version of the calculus features a new evaluation rule describing the behavior of the result structures and a call-by-value evaluation strategy. We prove the confluence of the obtained calculus and the correctness and completeness of the proposed encoding.

March 9 at 14:00
Sous-typage ensembliste avec types flèche et combinaisons booléennes, Alain Frisch (projet Cristal, Inria)

Les types CDuce sont purement structurels: ils ne font que décrire des ensembles de valeurs. La notion de sous-typage dans le langage correspond naturellement à l'inclusion ensembliste des types. En l'absence de types flèche, la théorie du sous-typage est bien connue puisque les types peuvent alors être vus comme des automates d'arbres et le sous-typage se ramène à l'inclusion des langages réguliers d'arbres. Les choses se compliquent avec les types flèche, c'est-à-dire lorsqu'on considère les fonctions comme des valeurs de première classe. En effet, on introduit alors des dépendences mutuelles entre la définition du sous-typage et le système de types du langage. D'un point de vue formel, on considère un système de types avec types récursifs, types flèche, combinaisons booléennes, et un lambda-calcul avec test dynamique de types et fonctions surchargées. Dans cet exposé, je présenterai les difficultés rencontrées et la méthode développée pour les contourner.

March 9 at 11:00
CDuce: un langage fonctionnel avec types et motifs pour XML, Alain Frisch

CDuce est un langage de programmation fonctionnel d'ordre supérieur avec un système de types et une opération de filtrage par motifs spécifiquement conçus pour XML. Dans cet exposé/demonstration, je présenterai les principaux traits du langages en insistant sur les motifs expression régulière, et je décrirai brièvement la structure du système de types.

February 9 at 14:00
Filtrage dans le lambda-calcul, modulo super-développements, Germain Faure

Traditionnellement, par filtrage d'ordre supérieur on entend filtrage d'ordre supérieur dans le lambda-calcul *typé*. Dans sa thèse, G. Sittampalam, propose de regarder le filtrage de manière différente : au lieu de restreindre l'ensemble des termes considérés, on restreint la notion de réduction (ici la beta-réduction). Nous proposerons une nouvelle lecture de ce travail en précisant : 1. la notion de réduction utilisée. Nous serons ainsi à même de définir clairement les problèmes de filtrage considérés et leurs propriétés (lien avec le filtrage du second ordre à la Huet-Lang). 2. l'algorithme utilisé : présentation synthétique sous forme de règles de transformation. Puis étude des propriétés de cet algorithme. La nouvelle lecture proposée ici met en avant un nouvel algorithme pour le filtrage du second ordre, en restreignant l'algorithme précédent (conjecture).

February 1 at 14:00
Typage de Xquery, Selina (王珍)

Lors de ses travaux de stage sur le typage de XQuery, Selina a réalisé un prototype en Tom.

January 25 at 14:00
Cadre générique pour les îlots formels, Emilie Balland

Cet exposé a pour thème la normalisation forte du lambda-calcul simplement typé avec réécriture. Nous présenterons un critère en cours de mise au point, qui a pour but but d'assurer cette propriété via un système de types. La particularité de ce système est qu'il utilise des types constraints qui permettent de manipuler des informations sur la taille des objets. Nous tenons à préciser que l'essentiel de ce qui est présenté est encore en cours de mise en place.

January 19 at 14:00
Normalisation forte du lambda-calcul simplement typé avec réécriture, Colin Riba

Cet exposé a pour thème la normalisation forte du lambda-calcul simplement typé avec réécriture. Nous présenterons un critère en cours de mise au point, qui a pour but but d'assurer cette propriété via un système de types. La particularité de ce système est qu'il utilise des types constraints qui permettent de manipuler des informations sur la taille des objets. Nous tenons à préciser que l'essentiel de ce qui est présenté est encore en cours de mise en place.

January 12 at 14:00
Anti-patterns, Radu Kopetz

J'expliquerai ce qu'est un anti-pattern, et comment résoudre le filtrage sur les anti-patterns en utilisant des règles de réécriture.

January 5 at 14:00
GOM, Antoine Reilles

L'outil GOM permet de prototyper rapidement et efficacement des langages.

2005

December 8 at 14:00
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms, Hans de Nivelle

We present a way of transforming a resolution proof of a first-order formula, which may contain Skolemization steps, into a first-order proof without Skolemization. The size of the proof increases only moderately (polynomially). This makes it possible to effectively translate the output of a resolution theorem prover into a proof that is purely first-order.

December 1 at 14:00
Application de la terminaison des systèmes de réécriture probabiliste, Florent Garnier

Nous utilisons une méthode de preuve sur les systèmes de réécriture probabiliste pour prouver la terminaison en temps moyen fini du protocole CSMA/CA 802.11b en mode infrastructure.

November 17 at 14:00
Global Computing et ARIGATONI, Luigi Liquori

November 10 at 14:00
Inférence stratifiée pour les types algébriques gardés, Yann Régis-Gianas

Les types algébriques gardés - ou généralisés - sont une extension des types algébriques présents dans les langages de programmation fonctionnelle de la famille ML. De nombreuses applications des types gardés ont été découvertes récemment. Toutes profitent de leur typage plus fin pour exprimer de puissants invariants statiques et rendre la programmation plus sûre.
L'inférence de type pour ML muni de types gardés est un problème complexe (certains programmes n'ont pas de type principal). Dès lors, seules des solutions incomplètes ont été proposées : l'inférence de type peut rejeter un programme bien typé si il n'est pas suffisamment annoté par le programmeur. Dans un tel contexte, il convient de définir clairement à quelle position les annotations de l'utilisateur doivent être rajoutées.
L'approche proposée par les auteurs est une "inférence de type stratifiée". La strate "noyau" est un ML étendu dans lequel le typage des types gardés est explicite (les annotations à insérer sont nombreuses mais clairement localisées). La strate "superficielle" est un algorithme d'inférence locale servant à propager les annotations de l'utilisateur. Ce dernier algorithme a un comportement prédictible ce qui est un point essentiel pour rendre robuste la programmation avec les types gardés.

November 3 at 14:00
[pdf] Systèmes Canoniques Abstraits : application à la complétion et à la déduction modulo, Guillaume Burel

Les Systèmes d'Inférence Canoniques Abstraits sont un cadre théorique introduit par N. Dershowitz et C. Kirchner pour formaliser une certaine notion de "bonne preuve". Ce cadre s'appuie principalement sur l'introduction d'un ordre sur les preuves, et les "bonnes preuves" sont alors les preuves minimales pour cet ordre. Ce cadre permet donc de traiter aussi bien la logique équationnelle, pour laquelle les bonnes preuves sont les preuves par réécriture (preuves en vallée), que les systèmes de séquents pour lesquels les bonnes preuves sont les preuves sans coupures.
Au cours de ce séminaire, je présenterai dans un premier temps les résultats que j'ai obtenu au cours de mon stage de mastère. J'y ai démontré que le cadre des Systèmes Canoniques Abstrait pouvait être appliqué a la complétion standard (Knuth-Bendix) ainsi qu'à la déduction naturelle.
Dans un deuxième temps, je présenterai quelques articles écrits par G. Dowek sur la déduction modulo asymétrique et polarisée. Ces travaux permettent d'établir un parallèle entre preuve en vallée et preuve sans coupure, entre confluence et propriété d'élimination des coupures et entre réduction de pic et normalisation. Ceci suggère la définition d'une procédure de complétion généralisée qui, appliquée a une théorie, la transforme de façon à ce que le système résultant possède la propriété d'élimination des coupures. Une telle procédure a été proposée par G. Dowek, mais celle-ci nécessite la recherche d'un modèle de la théorie considérée. Nous chercherons s'il n'existe pas une approche plus syntaxique à cette question.

October 28 at 11:00
Pure Pattern Calculus, Delia Kesner

The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any term to be a pattern. As well as supporting a uniform approach to functions, it supports a uniform approach to data structures which underpins two new forms of polymorphism. Path polymorphism supports searches or queries along all paths through an arbitrary data structure. Pattern polymorphism supports the dynamic creation and evaluation of patterns, so that queries can be customised in reaction to new information about the structures to be encountered. In combination, these features provide a natural account of tasks such as programming with XML paths. As the variables used in matching can now be eliminated by reduction it is necessary to separate them from the binding variables used to control scope. Then standard techniques suffice to ensure reduction progresses and to establish confluence of reduction.

October 28 at 11:45
Functors in SET: results and open problems, Furio Honsell

October 21 at 11:00
The graph rewriting calculus: properties and expressive capabilities, répétition soutenance de thèse de Clara Bertolissi

The last few years have seen the development of the rewriting calculus (also called rho-calculus) that uniformly integrates first-order term rewriting and lambda-calculus. This thesis is devoted to the study of the expressiveness of the rewriting calculus, with special interest for higher-order rewriting and the possibility of dealing with graph-like structures.
The first part of the thesis is dedicated to the relationship between the rewriting calculus and higher-order term rewriting, namely the Combinatory Reduction Systems (CRSs). First, an original matching algorithm for CRSs terms that uses a simple term translation and the classical higher-order pattern matching of lambda terms is proposed and then an encoding of CRSs in the rewriting calculus based on a translation of each possible CRS-reduction into a corresponding rho-reduction is presented.
The second part of the thesis is devoted to an extension of the rho-calculus, called graph rewriting calculus, handling terms with sharing and cycles. The calculus over terms is naturally generalised by using unification constraints in addition to standard rho-calculus matching constraints. The graph rewriting calculus is shown to be confluent over equivalence classes of terms, under some linearity restrictions on patterns, and expressive enough to simulate first-order term graph rewriting and cyclic lambda-calculus.

October 7 at 14:00
[pdf] Natural Deduction via Graphs, Herman Geuvers

We introduce the formalism of "deduction graphs" as a generalisation of both Gentzen-Prawitz style natural deduction and Fitch style flag deduction. The advantage of this formalism is that subproofs can be shared, like in flag deductions (and unlike natural deduction), but also that the linearisation used in flag deductions is avoided. Our deduction graphs have both "nodes" and "boxes", which are collections of nodes that also form a node themselves.
We give a precise definition of deduction graphs and we give examples to illustrate them. We also show the connections with other natural deduction formalisms. Gentzen-Prawitz style natural deductions and Fitch style flag deductions can easily be embedded into the deduction graph formlism. We study the computational behaviour of deduction graphs by analysing the process of cut-elimination and by defining translations from deduction graphs to simply typed lambda terms. From a slight variation of this translation we conclude that the process of cut-elimination is strongly normalising. The translation to simple type theory removes quite a lot of structure and we therefore also propose a translation to a context calculus with lets, that faithfully captures the structure of deduction graphs.

October 7 at 15:00
[pdf] Boxed Ambients with Communication Interfaces, Mariangiola Dezani

We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus allowing a liberal communication policy. Each ambient carries its local view of the topic of conversation (the type of the information being exchanged) with parents and children that will condition where it is allowed to stay or migrate to and which ambients may be allowed to enter it. The topic of conversation view of ambients can dynamically change during migration. BACI is flexible enough to allow different topics of conversation between an ambient and different parents, without compromising type-safety: it uses port names for communication and ambient names for mobility. Capabilities and co-capabilities exchange port names and run-time typing information to control mobility. We show the type-soundness of BACI proving that it satisfies the subject reduction property. Moreover we study its behavioural semantics by means of a labelled transition system.

October 7 at 16:00
[pdf] Intersection Types à la Church, Luigi Liquori

We present a fully typed lambda-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between the typed system and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both the type checking and type reconstruction are decidable.

September 29 at 16:30
[pdf] Typage et déduction dans le calcul de réécriture, répétition soutenance de thèse de Benjamin Wack

Le calcul de réécriture est un lambda-calcul avec filtrage. Cette thèse est consacrée à l'étude de systèmes de types pour ce calcul et à son utilisation dans le domaine de la déduction.
Nous étudions deux paradigmes de typage. Le premier est inspiré du lambda-calcul simplement typé, mais un terme peut y être typé sans être terminant. Nous l'utilisons donc pour représenter des programmes et des systèmes de réécriture. La seconde famille de systèmes de types que nous étudions est adaptée des Pure Type Systems. Nous en démontrons la normalisation forte grâce à une traduction vers le lambda-calcul typé.
Enfin nous proposons deux approches pour l'utilisation du calcul de réécriture en logique. La première consiste à définir des termes de preuve pour la déduction modulo à l'aide des systèmes fortement normalisants. Dans la seconde, nous définissons une généralisation de la déduction naturelle et nous montrons que le filtrage est utile pour représenter les règles de ce système de déduction.