Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq
In: https://hal.inria.fr/inria-00074332 ; [Rapport de recherche] RR-2345, INRIA. 1994, 1994
Online
report
Zugriff:
Projet COQ ; Nous présentons l'axiomatisation de la théorie du $\Lenv$-calcul dans le système Coq. Le principal résultat axiomatisé est la confluence de ce calcul. Par ailleurs, nous proposons un codage uniforme des systèmes de réécriture à une ou plusieurs sortes, sur lequel nous étudions la confluence locale.
Titel: |
Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq
|
---|---|
Autor/in / Beteiligte Person: | Saibi, Amokrane ; Formal Specifications and Program Validation (COQ) ; Paris-Rocquencourt, Inria ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; INRIA |
Link: | |
Zeitschrift: | https://hal.inria.fr/inria-00074332 ; [Rapport de recherche] RR-2345, INRIA. 1994, 1994 |
Veröffentlichung: | HAL CCSD, 1994 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|