Invited Talk: Type theory and recursion (at LICS 1993)
Authors: G. D. PlotkinAbstract
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 = {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} }