A-translation and looping combinators in pure type systems
- 1 January 1994
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 4 (1) , 77-88
- https://doi.org/10.1017/s0956796800000952
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.Keywords
This publication has 4 references indexed in Scilit:
- Modular proof of strong normalization for the calculus of constructionsJournal of Functional Programming, 1991
- Introduction to generalized type systemsJournal of Functional Programming, 1991
- Syntactic translations and provably recursive functionsThe Journal of Symbolic Logic, 1985
- Classically and intuitionistically provably recursive functionsPublished by Springer Nature ,1978