Seminars of the Protheo team - Year 2002-2003

2003

July 17, 2 pm:
Implementation of context matching, Vikram Krishnaprasad

Context Matching extends First Order Matching by allowing context variables along with individual term variables. Context variables can occur as monadic operators anywhere inside a term and can be instantiated by a context (a term with a single occurence of a hole). Context Matching, therefore, provides us with greater expressivity in describing context equations. Applications could be found in data querying and in term rewriting, where this could provide greater control in declaratively mentioning rewrite rules.
This talk would present and discuss an implementation of two context matching algorithms, one that was designed to solve linear context matching problems and another to solve generic ones. We would discuss the overall system design and the machinery needed to represent and manipulate terms with contexts and also talk about its performance. An interesting improvisation, which makes it possible to solve generic problems with the linear algorithm reasonably efficiently, will also be talked about.

July 16, 2pm:
Hériter des spécifications et des théorèmes - Une présentation du système FoC, Virgile Prevosto (LIP6)

FoC est un langage dédié au calcul formel certifié implanté au dessus de Ocaml et Coq. La hiérarchie de structures mathématiques offerte par FoC peut se décrire à l'aide d'une sémantique orienté-objet. Grosso modo, une structure algébrique correspond à une classe et une opération ou une propriété correspond à une méthode. Une structure peut être construite à partir de structures préexistantes par des mécanismes d'héritage. Toutefois, afin de garantir la correction de ces mécanismes, nous avons été amenés à définir un certain nombre d'analyses statiques (typage et calcul de dépendances). Par ailleurs, l'absence de mécanismes objets en Coq a conduit à proposer une traduction basée sur des enregistrements et des "générateurs de méthodes". Ces derniers sont des lambda-abstractions permettant de retrouver un des aspects essentiels (pour FoC) de la programmation objet, la liaison retardée. Durant cet exposé, on commencera par décrire l'analyse des dépendances entre méthodes telle qu'elle est faite en FoC. Nous verrons ensuite comment les constructions du langage de FoC se reflètent dans les classes et les modules de Ocaml. Enfin, nous nous intéresserons à la traduction en Coq, pour laquelle les résultats du calcul de dépendances s'avèrent indispensable. Pour conclure, nous montrerons comment cette traduction en Coq a inspiré une nouvelle traduction en Ocaml, n'utilisant pas la couche objet du langage, et nous comparerons les deux traductions en Ocaml en termes d'efficacité à l'aide d'exemples tirés de la librairie standard de FoC. Slides: [ps] [advi]

July 9, 2 pm:
A rule language for interaction, Christophe Ringeissen

We propose a rule language for designing interactive component languages and basic coordination languages. In our language, concurrent rules manage interactions and applications of call-back functions on a store of data that can freely be structured as an array, a list, a set of communication channels, etc. This rule language is a kind of abstract machine to write interactive component languages. We then propose a specific component languages to write solver cooperation languages. We illustrate the use of this language to specify and implement the cooperation language introduced by Castro and Monfroy (AISC'2000). Slides: [pdf]

July 2, 2 pm:
Coq tacticals and PVS strategies: a small step semantics, Florent Kirchner (INRIA Futurs, LogiCal). Slides: [pdf]

June 25, 2 pm:
Coopération de procédures de décision: étude et implantation, Duc-Khanh Tran

Les procédures de décision se trouvent au coeur de tous les outils modernes de l'analyse et la vérification des programmes car leur utilisation accroît d'une part l'efficacité du système de vérification et décharge d'autre part l'utilisateur de l'interaction, souvent fastidieuse, avec le système.
Néanmoins, la plupart des problèmes de vérification font intervenir des mélanges de différentes théories par exemples les listes, les tableaux et les réels. Pour résoudre ce genre de problème il est souhaitable de procéder de façon modulaire en faisant coopérer les procédures de décision connues sur les théories élémentaires.
Cette direction de recherche a été explorée pour la première fois il y a une vingtaine d'années grâce à des travaux précurseurs concernant la combinaison disjointe menés indépendamment par Shostak d'une part et Nelson-Oppen d'autre part dans le cadre de la vérification des programmes.
Nos objectifs dans le cadre du stage concernent d'une part, la reformulation dans un cadre plus uniforme de la combinaison des deux approches Nelson-Oppen et Shostak et d'autre part, la proposition des nouvelles procédures de combinaisons dans différents contextes spécifiques, par exemple la combinaison des théories de Shostak et des théories stable-infinies.
Nous réalisons également une expérimentation dans le système de vérification haRVey développé au sein de l'équipe Cassis.

May 28, 2 pm:
Termination of strategies in rule-based languages, Olivier Fissore

In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient criterion for ELAN-like strategies to terminate, only lying on rewrite rules involved in the strategy. We then give a simplification process of strategies, itself described by rewriting, to empower the previous criterion. This simplification can also make proofs of other program properties easier.

May 27, 10 am:
Rewriting modulo in Deduction modulo, Frédéric Blanqui (LIX)

We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computable closure for ensuring the termination of the combination of rewriting and beta-reduction. Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computable closure. This includes equations like associativity and commutativity, and provides an original treatment of termination modulo equations. Slides: [ps]

May 21, 2 pm:
Étude d'un bus logiciel basé sur la réécriture, Stéphane Hion. Slides: [ps]

May 7, 2 pm:
An imperative rewriting calculus, Luigi Liquori (INRIA Sophia Antipolis, Miro) (joint work with Bernard Paul Serpette)

We present an imperative version of the Rewriting Calculus, a pattern-matching based calculus with side-effects, which we call Imprho.
We formulate the static and dynamic semantics of Imprho. Because of the imperative aspects, a call-by-value operational semantics is given in the style of Kahn's Natural Semantics. The operational semantics is deterministic, and immediately suggests how to build an interpreter for the calculus. The static semantics is given via a first-order type system based on a form of (product-) conjunctive-types reflecting the (non-commutative) structure of the term.
The calculus is à la Church, in the sense that abstractions over patterns are decorated with contexts containing the types of the free variables of the pattern. In addition to the capability to access and modify a (monomorphic) typed store, the considered type system allows ``functional'' fixpoints, hence allowing the calculus to be trivially Turing complete. We show that Imprho enjoys subject reduction, type soundness, minimum typing, decidability of type checking and type reconstruction almost completely by a machine assisted approach, using the proof assistant Coq. Slides: [pdf]

April 16, 2 pm:
Évaluation concurrente et stratégies en TOM, Antoine Reilles. Slides: [pdf]

April 11, 1:30 pm:
Des fonctions discrètes aux fonctions réelles: comparaisons de quelques classes de fonctions, Emmanuel Hainry (ENS Lyon). Slides: [ps]

April 2, 2:30 pm:
Reachability analysis of process rewrite systems: application to the verification of multithreaded recursive programs, Tayssir Touili (LIAFA) (joint work with Ahmed Bouajjani)

We consider the verification problem of programs with unbounded (1) recursive procedure calls, and (2) dynamic creation of concurrent processes. Programs are modeled using term rewrite systems called PRS (for Process Rewrite Systems). These models are more powerful than pushdown automata and Petri nets, two common models for reasoning about, respectively, recursive programs without process creation, and multi-threaded programs without recursive calls. A PRS can actually be seen as the nesting of prefix rewrite system and a multiset rewrite system.
We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is semilinear. We represent PRS reachability sets by means of a new class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to new reachability analysis procedures for PRS.

March 26, 2 pm:
Jakarta: un environnement pour la certification de la plateforme JavaCard, Pierre Courtieu (INRIA Sophia Antipolis, Lemme). Slides: [ps]

March 19, 2 pm:
Assuring Secrecy for Concurrent Declarative Programs, Rachid Echahed (IMAG) (joint work with F. Prost and W. Serwe)

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses a terminating abstract operational semantics which reduces the problem of secrecy to constraint solving within finite lattices. It departs in that from the previous works essentially based on type systems. Furthermore, our proposal is general and tackles a very large class of programs, featuring dynamic process creation, general sequential composition, recursive process calls and high level synchronization.

March 12, 2 pm:
Réécriture d'ordre supérieur avec motifs, Julien Forest (LRI, Orsay)

We introduce a new higher-order rewriting formalism, called Expression Reduction Systems with Patterns (ERSP), where abstraction is not only allowed on variables but also on nested patterns. These patterns are built by combining standard algebraic patterns with choice constructors used to denote different possible structures allowed for an abstracted argument. In other words, the non deterministic choice between different rewriting rules which is inherent to classical rewriting formalisms can be lifted here to the level of patterns. We show that confluence holds for a reasonable class of systems and terms. Slides: [ps] [advi]

February 19, 2 pm:
Calcul de réécriture et (non-)terminaison, Benjamin Wack

The rewriting calculus embeds in a same setting the lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. Hence, the rewriting calculus can be thought as an extension of the lambda-calculus, and we are interested in the typed aspects. Here, we study extensively the polymorphic calculus à la Church, called Rho2. The calculus enjoy subject reduction, consistency of the normalizing terms and uniqueness of typing.
However, the considered type system does not prevent infinite reduction. In particular, by using pattern matching, one can encode (and typecheck) fixpoints, hence nonterminating programs. We illustrate on some examples (recursion, object encoding) how this gives the bases for a powerful functional language with powerful pattern matching facilities. Slides: [pdf]

February 12, 2 pm:
Éric Deplagne presents Emmanuel Kounalis and Pascal Urso's paper "Sound generalizations in mathematical induction" [ps]

February 5, 2 pm:
Complétude suffisante et terminaison innermost, Isabelle Gnaedig

In the context of a general approach of studying properties of rewriting under strategies, we focuss on the property of completeness of function definitions. We propose a procedure proving sufficient completeness of rewriting in the specific case of the innermost strategy, under the only assumption that the rewriting system innermost terminates on ground terms. It relies on an inductive proof that every ground term rewrites into a constructor term.

January 29, 2 pm:
Coopération Coq/ELAN dans la preuve par récurrence, Éric Deplagne, Claude Kirchner, Anamaria Martins-Moreira, Fabrice Nahon and Quang-Huy Nguyen

Nous présentons quelques résultats préliminaires dans l'utilisation d'ELAN pour automatiser ou semi-automatiser la récurrence par réécriture en Coq. L'idée est, à partir d'un énoncé Coq, de déterminer les variables de récurrence, le schéma d'instanciation et l'ordre noethérien utilisé avec aussi peu d'interaction avec l'utilisateur que possible. La preuve par récurrence est ensuite effectuée en ELAN qui génère un terme de preuve vérifiable par Coq. Nous prévoyons une démo de l'interface Coq/ELAN et abordons également les travaux restant à faire, qui sont nombreux. Slides: [pdf]

January 22, 2 pm:
Superposition with equivalence reasoning and delayed clause normal form transformation, Jürgen Stuber

We investigate a superposition calculus that optionally uses logical equivalences for rewriting instead of normalizing them to clause form (work in progress). Slides: [ps]

January 9, 2 pm:
L'outil haRVey, David Deharbe et Silvio Ranise (Cassis)

haRVery works in (a fragment of) first-order logic with equality. It automatically decides the validity of arbitrary boolean combination of ground literals modulo an equational theory (which is assumed to be axiomatized by a finite set of equational clauses). Examples of such theories are the theory of arrays, of lists, and their combination.
The system is based on a simple combination of BDDs (to compactly represent the boolean structure of ground formulae) and of superposition theorem proving (to effectively reason in the equational theories). If a formula is not valid, then some partial models contradicting it are returned.
So, the first face of haRVey deals with the propositional structure of the problem while the second face takes care of the reasoning in the (by now, equational) background theory.
haRVey is intended to be used as a component in larger verification systems, such as interactive theorem provers or symbolic simulators.
We have successfully used haRVey in the context of both software (namely, in the symbolic debugging and verification of imperative algorithms) and the verification of some hardware designs. We are now applying it in the context of invariant verification of concurrent systems.

January 9, 3 pm:
Direct combination of completion and congruence closure, Christelle Scharff

Theories presented by finite sets of ground (i.e. variable-free) equations are known to be decidable. There are different approaches to dealing with ground equational theories. Researchers interested in term rewriting, for instance, have applied completion, a method that transforms a given set of equations into a set of directed rules that is both terminating and confluent. Such a convergent rewrite system defines unique normal forms for equal terms and hence provides a decision procedure for the word problem of the underlying equational theory. Completion itself is a semi-decision procedure but under certain reasonable assumptions about the strategy used to transform equations, is guaranteed to terminate if the input is a set of ground equations.
A rather distinct approach to solving word problems for ground equational theories is based on the computation of the so-called congruence closure of a relation. Various efficient congruence closure algorithms have been proposed. They typically use a compact representation of the given terms by a directed acyclic graph. Completion methods are usually not as efficient, though one efficient ground completion method obtains an O(n log n) algorithm that cleverly uses congruence closure to transform a given set of ground equations into a convergent ground rewrite system. The standard completion approach is quadratic in the worst case.
We bridge the gap between the two approaches and provide a better understanding of the connection between completion and congruence closure by defining a new, efficient congruence closure method that integrates key ideas of completion and graph-based methods in a novel, direct and natural way. Our method takes its origin in the abstract congruence closure and the SOUR-graph method. It may be viewed as a modified version of the SOUR-graph approach, but with simpler graphs. In contrast to SOUR graphs it is not always possible to extract a (convergent) rewrite system from these graphs, but one always obtains a (partially constructed) abstract congruence closure, that is, a convergent rewrite system over an extended signature. Slides: [pdf]

2002

December 19, 10 am:
Tutoriel sur TOM, Pierre-Étienne Moreau

Qu'est ce que TOM ? Comment s'en servir ? Que peut-on faire avec ? Sous la forme d'exemples programmés en direct, le tutoriel tentera de répondre a ces questions.
En fonction de la demande, TOM peut etre installe sur des portables afin d'expérimenter certains exemples in live.

December 12, 2 pm:
Rewriting calculus: past, present, future, Horatiu Cirstea. Slides: [pdf]

December 5:
Application de la réécriture pour la génération automatique des mécanismes, Liliana Ibanescu

Notre travail se déroule dans le cadre du projet GasEl qui a comme but l'élaboration d'un logiciel de génération de mécanismes détaillés d'oxydation et de combustion de molécules d'hydrocarbures polycycliques.
Nous présenterons la notation interne des molécules et des réactions, la traduction des réactions élémentaires en règles de réécritures et l'utilisation des stratégies ELAN pour modéliser le mécanisme primaire. Slides: [ps]

December 4:
XML, transformations (web sémantique) et réécriture, Jérôme Euzenat (INRIA RhÔne-Alpes, EXMO)

XML est un language simple utilisé pour exprimer et diffuser des informations de toutes sortes. Les documents en XML sont amenés à être transformés, assemblés et réduits. XSLT a été développé afin d'exprimer des transformations. Il permet de définir un ensemble de règles (templates) pour réécrire des fragments d'arbres XML.
Si XSLT est un langage très bien adapté à l'expression de simples réécritures, il souffre d'un certain nombres de limitations: une stratégie d'évaluation fixée, déterministe et non réentrante (ou non cloturante?); l'impossibilité d'articuler plusieurs transformations dans le langage; la difficulté d'analyser le comportement des transformations à cause de constructeurs peu prédictibles (document()).
EXMO s'intéresse à l'échange et à la transformation de connaissance formalisée (i.e., décrite dans un langage doté d'une sémantique en théorie des modèles). Il a pour but d'établir des propriétés sémantiques (par exemple, la préservation des conséquences ou de la consistance) des transformations utilisées.
Afin de pouvoir analyser les transformations considérées, nous nous intéressons à la composition de transformations plus simples. Cela permet de répondre à l'un des défauts d'XSLT. Nous avons pour cela développé le système Transmorpher qui permet de décrire et d'exécuter de telles transformations. Notre but est de pouvoir associer des propriétés aux au transformations élémentaires et de prouver d'autres propriétés sur les transformations construites.
Parallèlement, il nous semble que les résultats acquis dans le domaine de la réécriture de termes ont un rôle à jouer dans la transformation de documents XML: parce qu'ils permettent de gérer un non-déterminisme faisant défaut à XSLT, parce qu'ils permettent l'expression de stratégies de réécriture variées et paramétrables et parce qu'ils permettent d'établir les propriétés computationnelles de systèmes de règles.
Mon but dans cet exposé est d'attirer, si c'était nécessaire, l'attention des praticiens de la réécriture sur un domaine d'application où ils ont beaucoup à apporter. Slides: [pdf]

November 28:
Safe recursion over an arbitrary structure: deterministic polynomial time, Paulin De Naurois

We provide several machine-independent characterizations of deterministic complexity classes in the model of computation proposed by L. Blum, M. Shub and S. Smale. We provide a characterization of partial recursive functions over any arbitrary structure. We show that polynomial time computable functions over any arbitrary structure can be characterized in term of safe recursive functions. We show that polynomial parallel time decision problems over any arbitrary structure can be characterized in terms of safe recursive functions with substitutions.

October 31st:
Fondements algébriques pour la réécriture, François Lamarche (Calligramme)

Nous donnons une définition algébrique abstraite de système de réécriture, qui permet:
- de traiter un grand nombre d'exemples de façon uniforme: termes ou graphes, avec ou sans equations, avec ou sans opérateurs de liage...
- de définir une théorie générale des dérivations, permettant entre autres de contrôler précisément quand deux d'entre elles peuvent être identifiées.
La base de notre approche est qu'un terme est un objet qui est sujet à différents types d'actions, entre autres:
- actions de renommage (substitutions de variables dans des variables)
- actions de substitution (substitutions de termes arbitraires dans des variables)
- actions de contraction/affaiblissement
- actions de liage
- actions de trace (utilisées par les calculs de processus).
Les actions de réécriture sont d'une nature différente, et elles forment un graphe (plus précisément, une catégorie) dont la structure « commute » avec les actions précitées. On peut prendre par exemple le graphe librement engendré par un ensemble de paires (l,r). On a donc un graphe de chemins, qui tient compte en plus des actions du paragraphe précédent. Mais ce graphe peut aussi être un ensemble ordonné noethérien, ce qui donne un système d'ordres de terminaison. Une preuve de terminaison pour un système du premier type S, c'est un homomorphisme de systèmes de réécriture S --> O dans un système du deuxième type.