Coding Simple Consensus Algorithm

Presented at the October 28, 2011 PRL Seminar

This Friday Bob, Mark and Vincent will illustrate how Event ML and Nuprl cooperate to produce correct-by-construction code for the Simple Consensus Algorithm. This example illustrates many features of Event Logic and of the practical use of Mark's notion of programmable event classes.

We will also illustrate how we can introduce diversity into the code at a high level and multiply it as we compile the protocol to production languages.

This Friday’s seminar will take place in Upson 5126 from Noon-1PM.

PRL Research Meeting: Posting Consensus Material to the Library

Join a discussion with the PRL team.

The PRL seminar for Friday Oct 21 will be a research meeting concerned with how to post proof material for simple consensus to the Library.  We will examine the formal material as written in Nuprl proofs and in EventML and consider the best ways of organizing this material in the library. Rich will display the material interactively to help focus the discussion.

This Friday’s seminar will take place in Upson 5126 from Noon-1PM.

There will be no PRL Seminar this week. We will resume next week Oct 21.

This month's Logical Methods in Computer Science (Vol 7 Issue 2) published an article by the PRL Group. The article Knowledge-Based Synthesis of Distributed Systems Using Event Structures by Mark Bickford, Robert Constable, Joseph Halpern, and Sabina Petride discusses... well rather than try to summarize it, here is the link and abstract:

Link: http://www.lmcs-online.org/ojs/viewarticle.php?id=496&layout=abstract

Abstract

To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.

The PRL Seminar for this Friday, October 7 will be Mark Bickford presenting Alexei Kopylov's work on the Image Type titled: Image Type: A New Type Constructor.

The seminar will take place in Upson 5126 from Noon-1PM.

Jim

There will be no PRL Seminar this week. We will resume next Friday, October 7.

JE

PRL Seminar for Friday Sept 23

Analyzing Access Control Logics Using Evidence Semantics

Presented by Robert Constable

It is known that access control logics can be given a clear semantics using realizability. Abadi has written about this as well as several other authors, and there is a mapping of Abadi's particular logic, CDD, into system F. However, in his paper Variations in Access Control Logic from 2008, he does not employ realizability.  I will interpret his results using evidence semantics because the proofs can be made simpler, they suggest implementation ideas, and because his results illustrate a principle that Mark and I advance: the natural logic of distributed computing is intuitionistic.

This week's seminar will take place in Upson 5126 from Noon-1PM.

PRL Seminar for Friday Sept. 16

NuPRL in Action

A demonstration by Mark Bickford

Mark Bickford will demonstrate the Nuprl system in action.  He will start by showing how to state and prove simple theorems in logic and number theory and extract efficient programs from the proofs.  He will also illustrate some elements of Event Logic in specifying a protocol. If there is time he will show some proofs he created this summer while tracking results of Dexter Kozen and Alexandra Silva as they were developing them. His investigations reveal a need to take a closer look at Brouwer's ideas about continuity as a general property of computable functions.

This week's seminar will take place in Upson 5126 from Noon-1PM.

This Friday's Seminar will feature a demonstration of NuPRL by Mark Bickford. Mark is a senior researcher on the PRL team focusing on proof development.

Details will be posted to the website later this week: http://www.nuprl.org/PRLSeminar/default.php

Jim

The Fall 2011 PRL Seminar begins today. This will be a planning meeting for the upcoming series.

We'll meet in Upson 5126 every Friday from Noon-1PM.

Please join us. Bring a brown bag lunch if you wish.

Updates on the seminar will be posted to http://www.nuprl.org/PRLSeminar/default.php

Jim

PRL Seminar Fall 2011

• Fridays Noon-1:00PM
• Meet in Upson Hall Room 5126
• Planning meeting set for Sept. 9

Coinciding with teaching EventML to students in our Formal Methods course, we have posted EventML for download on the CRASH Software page: http://www.nuprl.org/crash/software.php

There are Linux & PC install versions as well as a user's manual with background on Classic ML written by Kreitz & Rahli.

Jim

We've added a To Do List to the Wiki to capture and prioritize ideas for the PRL Project.

Link: To Do List

Jim

I got my first glimpse of EventML today. In the upcoming course on Formal Methods, Bob & Vincent will be teaching EventML. Today was the test of Vincent's installation for PC. We've got a smooth install ready for Win 7 & XP and will be sending it to the students in a week or so.

More info about EventML is on our CRASH project site.

Jim

The PRL Seminar will be held Fridays this fall (2011). Friday 9/9 will be an initial organizing meeting.

The Seminar will take place from Noon-1:00PM  in Upson Hall room 5126.

Please send questions or suggestions for the Seminar to Jim Entwood.

Jim

Details about the EventML software developed as part of the CRASH project were added to the website today.

The summary is at: http://www.nuprl.org/crash/software.php

Jim