DocumentCode
2894409
Title
Retracts in simply type λβη-calculus
Author
de´Liguoro, U. ; Piperno, A. ; Statman, R.
Author_Institution
Dipartimento di Sci. dell´´Informazione, Roma Univ., Italy
fYear
1992
fDate
22-25 Jun 1992
Firstpage
461
Lastpage
469
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
Keywords
data structures; formal logic; formal system; injections; isomorphisms; lambda -calculus; lambda calculus; linear lambda -terms; surjections; type lambda beta eta -calculus; Ear; Mathematical model; Mathematics; Remuneration; Time of arrival estimation; Virtual manufacturing;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location
Santa Cruz, CA
Print_ISBN
0-8186-2735-2
Type
conf
DOI
10.1109/LICS.1992.185557
Filename
185557
Link To Document