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.

• Type: Conference
• Year: 1987
• Where: CTCS
• Authors: Tatsuya Hagino
• Keywords: CTCS 1987, Lazy Types, Programming Languages, Recursive Types, Typed Lambda Calculus