PRL Website Update

Today we launched a major update for the PRL Project website. The update includes a new look and navigation as well as new content.

We have added:

• a knowledge base of all articles, math library books, and seminar presentations
• several new publications
• a formalized synthesized version of 2/3 Consensus
• a formalization in Nuprl of Moessner's theorem

What do you think?

We are looking for feedback, edits and comments. Please take a moment to complete our
quick survey or send comments by email to je277@cornell.edu.

Thanks!
PRL Project Team

PRL Seminar July 12: Intuitionistic Ancestral Logic

Join us on Thursday July 12 at noon for a PRL Seminar from Liron Cohen.

Liron will present her current work on Intuitionistic Ancestral Logic.

Details

Thurs. July 12
In Upson 5126
From Noon - 1PM

Summary

I will (informally) present a work in progress with Robert Constable on intuisionistic Ancestral Logic (iAL). We define iAL as an extension of iFOL, and illustrate its expressive power by relating it to omega logic with equality. A constructive proof for its consistency is given by showing that all provable formulas are realizable. The computational capabilities of iAL derive from the realizer for the computational induction principle over the transitive closure of a binary relation. I will show some examples of non-provable theorems of classical AL which turn out to be provable in iAL thanks to the realizers.

PRL Seminar for Today (5/11)

Recent Work with Coq

Presented by Mark Reitblatt

• Friday Noon-1:00PM
• Meet in Upson 215

There will be no PRL Seminar today.

Join us next week (5/11/12) for Mark Reitblatt's presentation of his recent work in Coq.

PRL Seminar for Friday April 20

Adding Shared Memory to the General Process Model

Presented by: Jason Wu

• Friday Noon-1:00PM
• Meet in Upson 215

We will discuss impredicative vs predicative type theory.  Bob will give an introduction and Mark will describe some new work he just finished and Rich Eaton is implementing to make it easier to manage the restrictions imposed by predicative theories like the computational type theory (CTT) of Nuprl.

Friday Apr 13 Noon-1:00PM

Meet in Upson 215

With a grant deadline pending we're cancelling PRL Seminar this week.

ACSU is holding their student/faculty lunch this Friday (3/30) so we've not holding the PRL Seminar.

We'll meet again the following week April 6.

The EventML page has moved to www.nuprl.org/software/ From this page we will post updates to the software and expanded tutorials and publications.

There will be no PRL Seminar this Friday (3/16/12).

Have a good spring break. We'll meet again on March 30.

PRL Seminar for March 9

Robert Constable leads a discussion: Reviewing Nuprl

• Friday Noon-1:00PM
• Meet in Upson 215

There will be no PRL Seminar today (3/2).

PRL Seminar for Feb 24

Join us 2/24 for a discussion of: Stronger Role for Recursive Types Needed in the Logic of Events

• Friday Noon-1:00PM
• Meet in Upson 215

No PRL Seminar this week (2/17/12).

Join us 2/24 for a discussion of: Stronger Role for Recursive Types Needed in the Logic of Events

Professor Constable has released a paperback version of Implementing Mathematics with the Nuprl Proof Development System. The book, written in 1985 by the PRL Team, serves as a manual to using the Nuprl system as well as an introduction to formal logic in computer science and its use in program development and verification.

The book is available from Amazon and other retailers.