Simply Typed Lambda-Calculus Modulo Type Isomorphisms

Abstract : We define a simply typed, non-deterministic lambda-calculus where isomorphic types are equated. To this end, an equivalence relation is settled at the term level. We then provide a proof of strong normalisation modulo equivalence. Such a proof is a non-trivial adaptation of the reducibility method.
Type de document :
Pré-publication, Document de travail
2014


https://hal.inria.fr/hal-01109104
Contributeur : Alejandro Díaz-Caro <>
Soumis le : lundi 15 juin 2015 - 00:25:42
Dernière modification le : mardi 16 juin 2015 - 01:08:59
Document(s) archivé(s) le : mardi 15 septembre 2015 - 14:15:42

Fichiers

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

Identifiants

  • HAL Id : hal-01109104, version 3
  • ARXIV : 1501.06125

Collections

Citation

Alejandro Díaz-Caro, Gilles Dowek. Simply Typed Lambda-Calculus Modulo Type Isomorphisms. 2014. <hal-01109104v3>

Partager

Métriques

Consultations de
la notice

179

Téléchargements du document

314