PRL Seminars

Logical programming environments (LPEs) are systems that support the program developer with a variety of logical tools. Nuprl-Light can be considered a LPE where the language of logical theories and the programming language are integrated using a common module system. Some of the features of the common system are reliability through verification, optimization through program transformation, and the ability to define domain-specific programming models.

In this seminar, I'll be covering the use of Nuprl-Light as a programming environment, and I'll provide examples from its application to the Ensemble group membership system. I'll also explore the remaining link in the implementation--the semantic connection between the logical theories and the O'Caml programming language. O'Caml is used to implement both Nuprl-Light and Ensemble.

Slides