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 : lundi 23 février 2015 - 16:22:47
Dernière modification le : mardi 16 juin 2015 - 01:08:59
Document(s) archivé(s) le : mercredi 27 mai 2015 - 10:01:59

Fichiers

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

Identifiants

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

Citation

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

Partager

Métriques

Consultations de la notice

110

Téléchargements de fichiers

32