Invited Paper: Type theory and recursion (at LICS 1993)

Authors: Gordon D. Plotkin

Abstract

Summary form only given. Type theory and recursion are analyzed in terms of intuitionistic linear type theory. This is compatible with a general recursion operator for the intuitionistic functions. The author considers second-order intuitionistic linear type theory whose primitive type constructions are linear and intuitionistic function types and second-order quantification

BibTeX

  @InProceedings{Plotkin-Typetheoryandrecurs,
    author = 	 {Gordon D. Plotkin},
    title = 	 {Type theory and recursion},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {374--374},
    location =   {Montreal, Canada}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }