A-Translation and Looping Combinators in Pure Type Systems

Thierry Coquand (1) , Hugo Herbelin (2)

1 Division of Computing Science
2 LIP - Laboratoire de l'Informatique du Parallélisme

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.

Mots clés: Pure Type Systems; Turing completeness; inconsistent formal systems; A-translation; continuation-passing-style translation; polymorphism; undecidability of type-checking

Domaines: Logique en informatique [cs.LO]

Thierry Coquand, Hugo Herbelin. A-Translation and Looping Combinators in Pure Type Systems. Journal of Functional Programming, 1994, 4 (1), pp.77-88. ⟨inria-00159085⟩