A-translation and looping combinators in pure type systems
Thierry Coquand, Hugo Herbelin · Journal of Functional Programming · 1994
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, a class which includes type systems with a type of all types. This is the first non-automated solution to this problem.