A-translation and looping combinators in pure type systems

DOI10.1017/S0956796800000952zbMath0817.03007MaRDI QIDQ4764266

Thierry Coquand, Hugo Herbelin

Publication date: 11 June 1995

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

generalization of \(A\)-translation to a class of pure type systemsinconsistent type systemslooping combinator

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Unnamed Item, Strong normalization from weak normalization in typed \(\lambda\)-calculi, Unnamed Item, Weak normalization implies strong normalization in a class of non-dependent pure type systems, An induction principle for pure type systems, On paradoxes in normal form, Type inference for pure type systems, Clocked lambda calculus

Cites Work

• Syntactic translations and provably recursive functions