Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:39:44 AM
Last modification on : Friday, February 4, 2022 - 3:22:31 AM


  • HAL Id : inria-00099645, version 1



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



Record views