Paper: Retracts in simply type λβη-calculus (at LICS 1992)

Authors: Ugo de'Liguoro Adolfo Piperno Richard Statman

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 = 	 {Ugo de'Liguoro and Adolfo Piperno and Richard Statman},
    title = 	 {Retracts in simply type λβη-calculus},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {461--469},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }