CS786 - Computational Type Theory

Wednesday, April 12, 2000

3:35 pm

Upson 5126

Stuart Allen

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

This week we continue with the explanations started last week about a non-type-theoretic semantics that attempts to imitate the structure of type theory. We discussed how types are represented, and how the inductive definitions are formulated, which support arguments by induction on type-formation.

Handouts for this topic were given out two weeks ago. 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 several meetings recently.

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