Logic in Computer Science (LICS 1992)

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}
  }