## A Typed Lambda Calculus with Categorical Type Constructors

**Tatsuya Hagino**
*Abstract:* 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.

*LFCS report ECS-LFCS-88-44*

Previous |

Index |

Next