PRL Seminar - since 1979

Join the PRL seminar email listerv and get updates on the PRL group and information about the next seminars. Send an email to
"join-prl-l@list.cornell.edu" with nothing in the body or subject to be automatically added.

Upcoming Seminars

List of Past Seminars »

with selected abstracts and slides.

PRL Seminar History

In 1979 we started a seminar which has been running ever since. The goal of the seminar for the first three years was to design a system for writing correct programs by progressive refinement. The result was the LambdaPRL system which evolved into Nuprl. Since that time the seminar has focused on research topics in constructive type theory, applied logic, formal methods, correct-by-construction programming, proof assistants for type theory, the use of proof assistants in programming, and related topics.

From time to time we have returned to focus on extending the type theory (CTT) and its Nuprl implementation. Starting in 2000 we worked on the development of Nuprl 5 and its Logical Programming Environment (aka Interactive Development Environment) including a Formal Digital Library (FDL). In 2012 we started the design of an internal distributed computation system.

We cover topics related to the project goals. There has been a consistent strong emphasis on topics in programming languages, formal methods, and automated reasoning. We are increasingly interested in using Nuprl as a programming language distributed protocols, and the EventML programming language introduced in 2011 is an experiment in connecting Nuprl to an ML-like programming language.