Title :
Type theory and recursion
Author_Institution :
Dept. of Comput. Sci., Edinburgh Univ., UK
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;
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
DOI :
10.1109/LICS.1993.287571
