DocumentCode
1822422
Title
Type theory and recursion
Author
Plotkin, G.D.
Author_Institution
Dept. of Comput. Sci., Edinburgh Univ., UK
fYear
1993
fDate
19-23 Jun 1993
Firstpage
374
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
Keywords
recursive functions; type theory; general recursion operator; intuitionistic function; intuitionistic function types; intuitionistic linear type theory; primitive type constructions; second-order quantification; second-order type theory; Algebra; Calculus; Computer languages; Computer science; Ear; Equations; Laboratories; Logic; Parametric statistics; Power system modeling;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location
Montreal, Que.
Print_ISBN
0-8186-3140-6
Type
conf
DOI
10.1109/LICS.1993.287571
Filename
287571
Link To Document