3:35 pm
Upson 5126
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
To be added to the mailing list for cs786 email sfa@cs.cornell.edu