CS786 - Computational Type Theory

Wednesday, Feb 9, 2000

3:35 pm

Upson 5126

Stuart Allen

Logical and Semantic Preliminaries

We will introduce standard logical concepts and issues upon which computational type theory will be brought to bear in later lectures.

Generic Issues:

Compositional reference of expressions

Functions and types

Identity

Well-formedness (judging that an expression has reference)

Issues of Constructivity:

Constructive meanings of propositions

Effective notations and computation

Computational content of proofs

To be added to the mailing list for cs786 email sfa@cs.cornell.edu