Sciweavers

Share
CTCS
1987
Springer

A Typed Lambda Calculus with Categorical Type Constructors

8 years 10 months ago
A Typed Lambda Calculus with Categorical Type Constructors
A typed lambda calculus with categorical type constructors is introduced. It has a uniform category theoretic mechanism to declare new types. Its type structure includes categorical objects like products and coproducts as well as recursive types like natural numbers and lists. It also allows duals of recursive types, i.e. lazy types, like infinite lists. It has generalized iterators for recursive types and duals of iterators for lazy types. We will give reduction rules for this simply typed lambda calculus and show that they are strongly normalizing even though it has infinite things like infinite lists.
Tatsuya Hagino
Added 28 Aug 2010
Updated 28 Aug 2010
Type Conference
Year 1987
Where CTCS
Authors Tatsuya Hagino
Comments (0)
books