Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00099418
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:02:47 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Friday, November 25, 2016 - 12:00:59 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

77

Files downloads

86