In this paper retractions existing in all models of simply typed lambda-calculus are studied relating them to other relations among types 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 lambda-terms and results aiming to a system complete w.r.t. the "provable retractions" tout court are established.

Retracts in simply typed λ-βη calculus

DE' LIGUORO, Ugo;
1992-01-01

Abstract

In this paper retractions existing in all models of simply typed lambda-calculus are studied relating them to other relations among types 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 lambda-terms and results aiming to a system complete w.r.t. the "provable retractions" tout court are established.
1992
IEEE-LICS '92
Santa Cruz, California, USA
22-25 Giugno 1992
Proceedings of IEEE-LICS '92
IEEE Computer Society Press
461
469
0818627352
Ugo de' Liguoro; Adolfo Piperno; Rick Statman
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/102144
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact