Working in a variant of the intersection type assignment system of Coppo...
Corrado Böhm once observed that if Y is any fixed point combinator (fpc)...
We prove that if A is a locally λ-presentable category
and T : A→A is a ...
The main observational equivalences of the untyped lambda-calculus have ...