KnowledgeBase » SEMINAR » ID = 427

Formal Module Systems and Nuprl-Light: A Programmer's Perspective

by Jason Hickey
1995-1996

Abstract

In this seminar we discuss an implementation of a Nuprl refiner (called "Nuprl-light") that provides an environment for modular proof development. During a PRL seminar last term, we developed the formal basis for modules in type theory (which consist of axioms and theorems that define a mathematical domain). The system we proposed allows new modules to inherit properties of existing modules using an object-oriented methodology.

In this self-contained seminar, we extend the module system to include informal objects that define domain-specific knowledge, such as theorem proving tactics and decision procedures. This development requires close interaction between the relatively informal module system provided by the programming language (in this case, Caml-special-light) and the formal modules provided by the Nuprl-light refiner.

Along the way, we will show how to develop theories as programming modules, and we will give several examples, from the definition of a type theory, to examples of theories-as-objects.