Aspects typés du calcul de réécriture

Benjamin Wack 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Le calcul de réécriture intègre dans un même système le lambda-calcul et la réécriture. Pour cela, les abstractions ne se font plus seulement sur des variables mais sur des motifs. On profite ainsi à la fois des mécanismes d'ordre supérieur du lambda-calcul et de l'expressivité du filtrage de la réécriture. Nous nous intéressons ici au rho-calcul en tant qu'extension du lambda-calcul et nous en étudions les aspects typés, l'objectif étant de mieux comprendre les relations entre ce calcul et les systèmes logiques et ainsi d'étendre l'isomorphisme de Curry-Howard. Notre étude se base sur une généralisation du cube de Barendregt, où les deux abstracteurs lambda et Pi sont unifiés en un seul. Il nous faut aussi tenir compte des nouveaux éléments du rho-calcul. Sous les bonnes conditions, nous parvenons ainsi à prouver la plupart des propriétés habituelles des calculs typés. Cependant, l'unicité du type n'est généralement plus valable, notamment à cause de l'unification des abstracteurs. Nous prouvons que l'unicité reste valide dans les deux systèmes les plus simples.
Type de document :
Rapport
[Stage] A02-R-175 || wack02a, 2002, 44 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099418
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:02:47
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 12:00:59

Fichiers

Identifiants

  • HAL Id : inria-00099418, version 1

Collections

Citation

Benjamin Wack. Aspects typés du calcul de réécriture. [Stage] A02-R-175 || wack02a, 2002, 44 p. 〈inria-00099418〉

Partager

Métriques

Consultations de la notice

49

Téléchargements de fichiers

30