Skip to Main content Skip to Navigation
Reports

Confluence de calcul à motifs

Pierre Caserta 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Dans ce rapport, nous proposons une preuve de confluence générique qui poura être instanciée pour les différents calculs. Pour cela, nous nous intéresserons au lambda-calcul dynamique qui axiomatise la manière dont l'abstraction est réduite. Nous utilisons cette preuve pour l'étendre au cas où le filtrage est fait modulo une théorie, ici la commutativité. Intuitivement il faut que le filtrage soit stable par substitution, par réduction et par équivalence. Nous caractérisons aussi une classe d'algorithmes de filtrage qui conduisent à des calculs non confluents.
Document type :
Reports
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/inria-00337931
Contributor : Horatiu Cirstea <>
Submitted on : Monday, November 10, 2008 - 11:27:54 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Monday, June 7, 2010 - 7:44:57 PM

File

rapport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00337931, version 1

Collections

Citation

Pierre Caserta. Confluence de calcul à motifs. [Rapport de recherche] 2008. ⟨inria-00337931⟩

Share

Metrics

Record views

270

Files downloads

145