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.

Vincent has updated the Introduction to EventML PDF to include recent changes to the software.

This tutorial document is available on our software page: http://www.nuprl.org/crash/software.php

PRL Seminar Feb. 10, 2012: A Discussion in Consensus

At this week's PRL seminar, Jason Wu leads guides us through One Half Consensus. We will demonstrate how it works and explore the different ways we can express this protocol in Event ML.

• Friday Noon-1:00PM
• In Upson 215

The PRL Team, lead by Mark Bickford, presented at the recent LADA workshop in Philadelphia. Slides and the position paper titled The Logic of Events, a framework to reason about distributed systems have been posted to the nuprl site.

The links are available from: http://www.nuprl.org/documents/Bickford/LOE-LADA2012.html

EventML ver0.2, our continuing work in progress, has been updated and posted to the software page on PRL's CRASH site:

http://www.nuprl.org/crash/software.php

Updates includes fixdpoint operator and the ability to turn off the type checker.

Recursion and Co-induction in specifying protocols

We will look closely at an idea from Robbert VanRenesse for adding recursion/co-induction, as a combinator for event classes. We will explore the concept in general and use it to provide an alternative specification of Simple Consensus. We might also discuss the concept of how to obfuscate protocols using synthesis.

PRL Seminar

• Fridays Noon-1:00PM
• Note Room Change: Meet in Upson 215