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
Liste complète des métadonnées

https://hal.inria.fr/hal-01109104
Contributeur : Alejandro Díaz-Caro <>
Soumis le : samedi 24 janvier 2015 - 15:59:18
Dernière modification le : mercredi 25 février 2015 - 01:01:51
Document(s) archivé(s) le : samedi 25 avril 2015 - 10:12:35

Fichiers

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

Identifiants

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

Citation

Alejandro Díaz-Caro, Gilles Dowek. Simply Typed Lambda-Calculus Modulo Type Isomorphisms. 2014. 〈hal-01109104v1〉

Partager

Métriques

Consultations de la notice

141

Téléchargements de fichiers

12