Paper: The strength of the subset type in Martin-Löf's type theory (at LICS 1988)

Authors: Anne Salvesen Jan M. Smith

Abstract

The authors show that the exact formulation of the rules of type theory is important for rules of subset type. It turns out that there are propositions involving subsets that are trivially true in naive set theory, but which cannot be proved in type theory. They examine the probability of a type proposition that is important when modularizing program derivations

BibTeX

  @InProceedings{SalvesenSmith-Thestrengthofthesub,
    author = 	 {Anne Salvesen and Jan M. Smith},
    title = 	 {The strength of the subset type in Martin-Löf's type theory},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {384--391},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }