Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >
Please use this identifier to cite or link to this item:
|Title: ||Type Theory and Recursion Extended Abstract|
|Authors: ||Plotkin, Gordon|
|Issue Date: ||5-Nov-2003|
|Abstract: ||At first sight, type theory and recursion are compatible: there are many models of the typed lambda
calculus with a recursion operator at all types. However the situation changes as soon as one considers
sums. By a theorem of Huwig and Poign´e, any cartesian closed category with binary sums and such a general recursion operator is trivial. Domain theory provides the category of cpos and continuous functions.
It is cartesian closed and has a general recursion operator — the least fixed-point operator. It (necessarily)
does not have binary sums, but the closely associated
category of cpos and strict continuous functions does.
has derivable in System F finite products and sums,
second-order existential quantification and initial and
final algebras (of definable covariant functors). It is
both interesting — and necessary for the development
of the semantics of programming languages — to consider the interaction of polymorphism and recursion.
However as the parametric models have categorical
sums, a now familiar difficulty arises.
We consider instead a second-order intuitionistic
linear type theory whose primitive type constructions
are linear and intuitionistic function types and second-order quantification.|
|Keywords: ||Laboratory for Foundations of Computer Science|
|Appears in Collections:||Informatics Publications|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.