CS786 - Computational Type Theory

Wednesday, April 5, 2000

3:35 pm

Upson 5126

Stuart Allen

Non-type-theoretic imitation of type-theoretic semantics.

I will start explaining a non-type-theoretic semantics that attempts to imitate the structure of type theory. This material is precise and technical, but elementary. It will take more than one meeting, probably two.

Handouts for this topic were given out last week. This included TR87-832.

Types are symmetric, transitive relations on terms.

Type systems are recursively defined to assign "names" or "descriptions" to types.

Type systems with Universes are defined systematically from type system constructors.

Facts about types are proved by induction over universe level and type formation.

Christoph Kreitz spoke for the last few meetings.

Prior to that I had spoken:

2/23 Computational Theory and Nuprl

2/16 Computational Theory of Semantic Types

2/9 Logical and Semantic Preliminaries

Lecture notes from 2/9.(postscript text)

To be added to the mailing list for cs786 email sfa@cs.cornell.edu