CS786 - Computational Type Theory

Wednesday, April 19, 2000

3:35 pm

Upson 5126

Stuart Allen

Universes.

We will start by incorporating the definition of Universes into the non-type-theoretic semantics explained in the last two meetings (4/12 4/5 ). This material is in the handout from the last couple of sessions, which included TR87-832.

We'll also discuss universe polymorphism. This material is in TR87-866.

Then we'll return to a type-theoretic account of universes -- I'll propose that there are no universes, that universe construction is hypothetical.

Christoph Kreitz spoke for 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