A-Translation and Looping Combinators in Pure Type Systems

Abstract : We present here a generalization of A-translation to a class of Pure Type Systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of inconsistent type systems including type systems with a type of all types. This is the first non-automated solution to this problem.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 1994, 4 (1), pp.77-88
Liste complète des métadonnées

https://hal.inria.fr/inria-00159085
Contributeur : Hugo Herbelin <>
Soumis le : lundi 2 juillet 2007 - 11:44:33
Dernière modification le : mardi 24 avril 2018 - 13:53:09
Document(s) archivé(s) le : jeudi 8 avril 2010 - 22:15:16

Fichiers

jfp-CoHer94-looping.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00159085, version 1

Collections

Citation

Thierry Coquand, Hugo Herbelin. A-Translation and Looping Combinators in Pure Type Systems. Journal of Functional Programming, Cambridge University Press (CUP), 1994, 4 (1), pp.77-88. 〈inria-00159085〉

Partager

Métriques

Consultations de la notice

132

Téléchargements de fichiers

434