Calcul de réécriture explicite

Germain Faure 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The contributions of this report are twofold. First, we will give the intuition of how programs can be represented in the rewriting calculus. We will compare with the lambda-calculus and take many examples of OCaml programs. Secondly, we propose, study and exemplify a rewriting calculus with explicit constraint handling. In this calculus, matching and application of substitutions become explicit. The approach is really modular, allowing extension to arbitrary matching theories. We will also prove that the calculus is powerful enough to deal with errors. We will afterwards prove the confluence of the calculus and the termination of the ``explicit'' part of the calculus, some non trivial proofs. We conclude by an other extension of the calculus to handle composition of substitutions.
Type de document :
Rapport
[Intership report] A03-R-324 || faure03a, 2003, 40 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099645
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:39:44
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099645, version 1

Collections

Citation

Germain Faure. Calcul de réécriture explicite. [Intership report] A03-R-324 || faure03a, 2003, 40 p. 〈inria-00099645〉

Partager

Métriques

Consultations de la notice

119