KnowledgeBase » SEMINAR » ID = 715

An Extension of OCaml's Type Theory

by Robert L. Constable
2013

For this PRL Seminar, Bob Constable will discuss his plans for giving two or three lectures in CS3110 about an hypothetical extension of OCaml's type theory to Extended OCaml. The theory will have dependent types and equality for all types. It will become apparent to the class that this language can express logic, and he hopes to make "propositions as types" a revealed principle of type theory.

Nuprl is a good basis for this because it has partial as well as total types. On the other hand, we are only now starting to understand this mixed theory of total and partial types thoroughly.

The hope is for this seminar to be a discussion of the general idea of doing this in which ideas for how to teach it could be explored.

Date: October 23, 2013
Time: 4-5pm
Location: Upson 5130