Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

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

Authors: G. D. Plotkin


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


    author = 	 {G. D. Plotkin},
    title = 	 {Type theory and recursion},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {374--374},
    location =   {Montreal, Canada}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}