Paper: Equality Between Functionals in the Presence of Coproducts (at LICS 1995)

Authors: Daniel J. Dougherty Ramesh Subrahmanyam

Abstract

Consider the simply-typed lambda calculus with sum-type constructors, and let Set be the standard set-theoretic model of this calculus over an infinite base set. We present a proof system for the calculus (which involves a rule for reasoning by cases) and prove it to be a complete axiomatization of the equational theory of Set. We also develop some results concerning the syntactic properties of the calculus and an interpretation in Set of the equational theory (in the language of the classical simply- typed calculus) of the full function hierarchy over one infinite and one finite base set.

BibTeX

  @InProceedings{DoughertySubrahmany-EqualityBetweenFunc,
    author = 	 {Daniel J. Dougherty and Ramesh Subrahmanyam},
    title = 	 {Equality Between Functionals in the Presence of Coproducts},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {282-291},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }