Nested Data Types in polymorphic type theory and dependent type theory

Peter Aczel

Nested Data Types were introduced in the context of functional proramming languages like Haskell. They have also been studied in the context of the impredicative polymorphic type theory, system F^omega. But they can also be represented in weak predicative dependent type theories.

My talk will introduce the topic with some of the standard examples, including the nested dtat type treatment of the de Bruijn approach to the syntax of the untyped lambda calculus.
Thursday 5th June 2003, 15:00
Robert Recorde Room
Department of Computer Science