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.
Type de document :
Rapport
[Rapport de recherche] 2008
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00337931
Contributeur : Horatiu Cirstea <>
Soumis le : lundi 10 novembre 2008 - 11:27:54
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : lundi 7 juin 2010 - 19:44:57

Fichier

rapport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00337931, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

244

Téléchargements de fichiers

78