3:35 pm
Rhodes 508 (At Theory Center Elevator Shaft)
SPECIAL PLACE this time.
Computational Theory of Semantic Types
Type theory versus particular rules or type definitions
Type theory as a fragment of a theory of reference
Core claims of computational type theory
Standard types employed by those who apply type theory
Newer types of practical or theoretical value
Immediate constituent types of a type
Several related notions of "type"
Universes (introduction; foundations will be discussed later)
Computational content of proof
Previous week's cs786 - Logical and Semantic Preliminaries
Previous week's lecture notes.(postscript text)
To be added to the mailing list for cs786 email sfa@cs.cornell.edu