CS786 - Computational Type Theory

Wednesday, Feb 23, 2000

3:35 pm

Upson 211 (where PRL seminar usually is; BOOM had our room)

Stuart Allen

Computational Type Theory and Nuprl

Last week's intended topics were not all covered. This week we'll treat most of those leftovers as well as discuss semantics of Nuprl's sequents and a few rules. Theoretical issues will be treated aphoristically, leaving more discursive elaboration to notes and later classes. Some admonitions about likely misconceptions will be offered.

Standard types employed by those who apply type theory

Newer types of practical or theoretical value (maybe we'll put this off)

Universes (introduction; foundations will be discussed later)

Computational content of proof

Truth of Nuprl sequents (operator definitions and universe level variables)

Rules (validity, direct computation, universe polymorphism)

Previous week's cs786 Announcement - Computational Theory of Semantic Types

Notes for last week's lecture will be prepared, to the effect of ``what I should have said was ...'', to compensate for some vagueness and lack of emphasis in lecture.

Announcement for 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