Skip to Main content Skip to Navigation

# Calcul de réécriture explicite

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.
Mots-clés :
Document type :
Reports
Domain :
Complete list of metadata

https://hal.inria.fr/inria-00099645
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:39:44 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

### Identifiers

• HAL Id : inria-00099645, version 1

### Citation

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

Record views