Seminars of the Protheo team - Year 2003-2004

2004

June 17-18:
Nancy-Saarbrücken workshop on logic, proofs and programs

June 14, 10 am:
Liliana Ibanescu's PhD thesis defense on rule-based programming and strategies for automated generation of detailed kinetic models for gas phase combustion of polycyclic hydrocarbon molecules

June 10, 10 am:
Guillaume Darmont, Sébastien Hinderer and Stéphane Hrvatin present their master thesis works
  • Guillaume Darmont: transformations XML dans un environnement typé

    Depuis l'année dernière, TOM permet d'effectuer des transformations sur les documents XML. Afin d'en sécuriser l'écriture, il est nécessaire de mettre en place des algorithmes permettant de typer statiquement les programmes TOM. Utilisant le filtrage de liste existant dans TOM, le résultat obtenu est un algorithme servant à créer des programmes externes de validation de programme.

  • Sébastien Hinderer: formalisation en Coq de la preuve de terminaison des systèmes de réécriture par interprétations polynomiales.

    On montrera comment les diverses notions qui interviennent en réécriture du premier ordre, ainsi que les polynômes à n indéterminées ont été formalisés en Coq. Dans une seconde partie, nous évoquerons l'interface avec CiME qui a été développée pendant ce stage, et permet d'automatiser la recherche d'une interprétation polynômiale et la construction d'une preuve de terminaison pour un système de réécriture donné.

  • Stéphane Hrvatin: structuration et paramétrisation pour un outil de compilation de la réécriture

    Depuis sa création, Tom a eu une évolution qui le tend à s'approcher de plus en plus des langages de spécifications. Il est possible de créer des signatures (au sens algébrique du terme) et des règles de réécriture. Il manque cependant à Tom des outils permettant la structuration de spécifications comme l'extension ou la possibilité d'écrire des spécifications génériques. Ce stage de DEA a pour but de tester la possibilité d'avoir un tel outil en Tom qui utiliserait des outils déjà développés.

May 27, 2 pm:
Fabrice Nahon presents Pierre Corbineau's work on theorem proving

Il s'agit d'une extension naturelle du calcul LJT de Dyckhoff et il satisfait les propriétés d'élimination des coupures et des contractions, étendant ainsi les résultats obtenus par Dyckhoff, afin de justifier son utilisation comme base pour des procédures de recherche de preuves. Enfin, on décrit les stratégies mises en oeuvre dans l'implantation d'une tactique Coq basée sur ce calcul.

May 19, 9 am:
Réécriture de graphes avec redirection de pointeurs, Colin Riba (ENSIMAG)

Les structures de donnees a base de pointeurs se representent aisement sous forme de graphes. Afin de manipuler directement de telles structures dans les langages de programmation logico-fonctionels, une classe de systemes de reecriture de graphes dite admissible a deja ete proposee, et des resultats de confluence et de surreduction ont ete obtenus. Dans l'objectif de manipuler des structures cycliques, notre travail a ete d'etendre cette reecriture en y ajoutant une operation de redirection de pointeurs. Cet ajout nous conduit aux limites de la declarativite car il s'acompagne de la perte de la confluence dans le cas general. Cela nous a amene a proposer une strategie de reecriture basee sur la confluence des systemes admissibles etudies auparavant.

May 17, 10:20 am:
Probabilistic extentions of the Milner CCS process algebra, Florent Garnier

May 13, 2 pm:
Generating minimal conflict sets for linear arithmetic and uninterpreted functions, Duc Tran

We consider the problem of extending satisfiability procedures with the capability of returning ``small'' conflict sets when unsatisfiability is reported. In our setting, a minimal conflict set is an unsatisfiable set of constraints such that all its (strict) subsets are satisfiable. As an illustration, we propose an algorithm based on Gauss elimination to build minimal conflict sets or justification of equalities for the theory of linear equalities and disequalities over the rationals (or the reals). The theory of equality seems to be another good candidate due its simplicity and importance in verification. Unfortunately, enhancing a satisfiability procedure based on congruence closure with the capability of producing minimal conflict sets turns out to be surprisingly difficult. This procedure, as well as the Nelson-Oppen combination procedure, is often quite sensitive to the order in which the literals are processed or new (entailed) equalities are derived. However, we give a formal characterization of the weaker forms of minimality we can expect from proof-generating decision procedures introduced for the theory of equality and for its combination with linear arithmetic.

May 5, 10:30 am:
Scott domains for the rho-calculus, Germain Faure

Dans ce séminaire il ne sera pas question d'aborder les problèmes liés à l'étude de l'interprétation du rho-calcul dans les domaines de Scott. En revanche, j'essaierai de motiver et d'introduire une telle étude en commençant par la présenter pour le lambda-calcul. Ensuite, j'expliquerai en quoi notre travail (loin d'être abouti) m'a amené à identifier des points à préciser dans l'étude générale du rho-calcul.

May 5, 11:15 am:
Certification of pattern-matching compilation, Antoine Reilles

On s'intéresse à fournir un témoin de la validité de la compilation d'un problème de filtrage.

April 29, 2 pm:
Protheo meeting

March 24, 3:30 pm:
Clara Bertolissi presents Aiola and Klop's paper "Cyclic lambda graph rewriting" [ps]

Term graph rewriting is a well-known technique for implementing functional languages based on term rewriting. One possible approach to term graph rewriting consists in using an equational framework (Ariola and Klop, 1996) that models lambda calculus extended with explicit recursion: (cyclic) lambda graphs are treated as a system of recursion equations involving lambda terms; term graph rewriting is described as a sequence of equational transformations. In this kind of system, the confluence property breaks down, but can be restored by introducing a restraining mechanism on the substitution operation.

March 11-12:
Workshop on rho-calculus

February 26, 2 pm:
Germain Faure presents Aaron Stump's paper "An introduction to MicroRogue" [pdf]

February 19, 2 pm:
Typing programs with matching on topological collections, Julien Cohen (LaMI, Evry).

Les collections topologiques permettent de considérer uniformément de nombreuses structures de données dans un langage de programmation. Par exemple des tableaux, des graphes, des séquences, des ensembles ou des arbres peuvent être vus comme des collections topologiques. Elles sont manipulées par des fonctions définies par filtrage appelées des transformations.
Nous proposons deux systèmes de types pour des langages intégrant les collections topologiques et les transformations. Le premier est un système à la Hindley/Milner qui peut être entièrement typé à la compilation. Le second est un système mixte statique/dynamique permettant de traiter des collections hétérogènes, c'est-à-dire qui contiennent des valeurs de types distincts. Dans les deux cas l'inférence de types automatique est possible. Slides: [pdf] [advi]

February 12, 2 pm:
The suspension notation of explicit substitutions, Gopalan Nadathur (University of Minnesota)

Lambda terms have been used in the capacity of data structures in a variety of programming systems such as metalanguages, proof assistants and typed intermediate languages in recent years. New requirements have to be met by the representation of such terms in the implementation of such systems. Explicit substitution calculi provide a framework for realizing many of these requirements. In this talk we will describe the suspension notation of Nadathur and Wilson that is one example of such a calculus. This notation has similarities to the lambda sigma calculus: it permits the composition of reduction substitutions and is confluent over term metavariables. At a practical level, this notation has been used in two significant systems: the Standard ML of New Jersey compiler and the Teyjus implementation of Lambda Prolog. We will motivate the structure of this notation, discuss its relationship to other calculi and highlight some of its facets that are relevant to its deployment in actual systems.

January 22, 2 pm:
Florent Garnier presents Kumar, Sen, Meseguer and Agha's work on models of probalistic rewriting.

Le modèle de théories de réécritures probabilistes est une structure sémantique ayant pour vocation d'exprimer de manière générale un large spectre de systèmes. Je vous présenterai ce modèle ainsi que ce qu'en attendent ses auteurs, puis nous discuterons de la faisabilité de la mise en place d'une telle structure ainsi que de l'ensemble des applications pouvant en découler que ce soit du point de vue théorique ou appliqué. Slides: [pdf]

2003

December 18, 2 pm:
Termination checking with subtyping, Frédéric Blanqui

Je présenterai les derniers résultats auxquels j'ai aboutis quant à la terminaison de la combinaison de la récriture d'ordre supérieur et de la beta-réduction dans le Calcul des Constructions. Ce travail étend les travaux d'Abel sur le système F avec types inductifs, et de Barthe, Frade, Gimenez, Pinto et Uustalu sur le lambda-calcul simplement typé avec types inductifs, au cas des définitions par récriture (au lieu des définitions inductives à la ML) d'une part, et aux types dépendants d'autre part. Le critère de terminaison est simple et compatible avec la notion de cloture de calculabilité. Il unifie également la manière dont sont traités les arguments du "premier ordre" et ceux "d'ordre supérieur". J'essaierai également d'aborder les nombreuses questions et possibilités que ce critère de terminaison crée. [ps]

December 3, 2 pm:
Olivier Fissore's PhD thesis defense on termination of rewrite systems under strategies

November 27, 2 pm:
Higher-order matching in linear lambda-calculus, Sylvain Salvati (Calligramme).

Les problèmes d'unification sont très étudiés en informatique théorique car ils permettent l'automatisation de raisonnements symboliques. La plupart des problèmes d'unification du lambda calcul simplement typé sont indécidables (unification d'ordre 2 [Goldfarb], filtrage d'ordre 6 [Loader]...). Pour contourner cette difficulté, de nombreuses restrictions du problème ont été étudiées (Higher-order Patterns [Miller, Nipkow], unification de contexte, filtrage d'ordre 2 [Huet], d'ordre 3 [Dowek, Comon]...). Celle que je vais vous présenter est une restriction sur le calcul.
Nous nous plaçons dans le cadre du lambda calcul linéaire (calcul associé à la logique linéaire sans les exponentielles (MALL) par l'isomorphisme de Curry-Howard). Ce calcul est très peu puissant, mais, à ma connaissance, c'est le seul pour lequel le filtrage d'ordre supérieur soit décidable sans restriction.
Je présenterai :
1/ succinctement la logique linéaire et le lambda-calcul linéaire (structures multiplicatives, additives...)
2/ les résultats obtenus par Philippe de Groote (RTA'00) quant à la décidabilité et la complexité du filtrage pour ce calcul dans le cas où les types se limitent aux multiplicatifs.
3/ le fait que ce problème reste difficile (NP-complet), même dans des cas qui pourraient sembler simples à priori (Philippe de Groote, Sylvain Salvati, RTA'03)
4/ et enfin, des résultats récents (non publiés) qui montrent que le problème de filtrage reste décidable si on étend le calcul avec les additifs. Slides: [pdf]

November 20, 2 pm:
Semantics of the Calculus of Constructions, Alexandre Miquel (PPS, Jussieu)

Dans cet exposé, je présenterai les principaux outils de sémantique utilisés pour démontrer les propriétés de cohérence et de normalisation forte pour les systèmes de types de la famille des PTS (théorie des types), en prenant pour exemple l'étude du Calcul des Constructions, le formalisme sous-jacent au système Coq.
Dans une première partie, j'effectuerai la construction du modèle ensembliste du Calcul des Constructions dans lequel tous les termes de preuve sont identifiés (modèle classique, ou "proof-irrelevant"), lequel permet d'établir la cohérence logique du formalisme, sans passer par la normalisation forte. Je montrerai également les techniques qui permettent d'interpréter des extensions du formalisme telles que la hiérarchie d'univers.
Dans une deuxième partie, je montrerai comment les techniques de réalisabilité permettent d'incorporer des candidats de réductibilité au sein du modèle de manière à transformer la preuve de cohérence en preuve de normalisation forte.

September 25, 11 am:
Termination by resources, Jean-Yves Moyen (Calligramme)

La terminaison par ressource est une technique de preuve de terminaison d'algorithmes. Elle s'inspire du Size Change Principle de Neil Jones mais prend en compte de manière plus fine les changements de taille des variables, et donc ce que deviennent les ressources. Pour ce faire, on transforme le programme en réseau de Pétri et de l'analyse du réseau de Pétri découlent des propriétés du programme.
Il est très intéressant de remarquer que cette analyse permet aussi de détecter les programmes "Non Size Increasing" tels que définis par Martin Hofmann, et semble aussi utiliser des choses proches de plusieurs autres techniques d'analyses de programmes.
Un autre avantage de cette technique est qu'elle permet de travailler directement sur un langage proche d'un langage machine très simplifié. Elle serait donc utilisable par n'importe quel langage, après compilation, et non pas avant comme c'est le cas de beaucoup de techniques travaillant sur des langages fonctionnels. [ps]

September 24, 2 pm:
Development of Java+Tom programs in the Eclipse environment, Pierre-Étienne Moreau and Julien Guyon