A collection of PRL Project related news.
These news items, posted through Jim's Blog, also are featured on the www.nurprl.org home page feed.
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
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.