Paper: Retracts in simply type λβη-calculus (at LICS 1992)
Authors: de'Liguoro, U. Piperno, A. Statman, R.Abstract
Retractions existing in all models of simply typed λ-calculus are studied and related to other relations among types, such as isomorphisms, surjections, and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear λ-terms. Results aiming at a system complete with respect to the provable retractions tout court are established
BibTeX
@InProceedings{deLiguoroPipernoSta-Retractsinsimplytyp, author = {de'Liguoro, U. and Piperno, A. and Statman, R.}, title = {Retracts in simply type λβη-calculus}, booktitle = {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992}, year = 1992, editor = {Andre Scedrov}, month = {June}, pages = {461--469}, location = {Santa Cruz, CA, USA}, publisher = {IEEE Computer Society Press} }