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

The PRL Seminar will continue through the spring semester. Our next meeting will be Feb. 3, 2012.

The location has changed to Upson 215. The time is the same, meeting Fridays Noon-1:00PM.

If you are interested in presenting at the PRL Seminar please contact Jim - je277@cornell.edu. More info about the Seminar is on the PRL website

Cornell has a new website called Cloud Computing @ Cornell that highlights cloud computing research throughout the University.

The PRL Project plays a role in cloud research by developing and testing distributed protocols using formal proofs.

Lately we have had a lot of activity around EventML, the programming language Vincent Rahli has developed. We are refining EventML and exploring the potential of this programming language that uses Event Logic for coding distributed protocols and docks with the Nuprl theorem prover.

Yesterday a new version of the software package was released. It is available on our CRASH page:

www.nuprl.org/crash/software.php

We have also posted a draft Tutorial for EventML, including:

• Background about EventML
• Description of Event Classes
• Examples
  • Ping Pong
  • Leader Election in a Ring
  • Two-thirds Consensus

Discussion of the Nuprl Evaluator

Following up on the direction of last week’s extended seminar, today we will be continuing our discussion of the Nuprl evaluator.

This Friday’s seminar will take place in Upson 5126 from 12:05-1:00PM.

We had a lively discussion at the Seminar Last week following Chung-chieh Shan's talk.

Slides from the talk are available at:

http://www.nuprl.org/PRLSeminar/PRLSeminar2011/Chung-chiehShan-FinallyTaglessPartiallyEevaluated.pdf

Coming up this Friday (Dec. 9) will be a discussion of the Nuprl Evaluator.

PRL Seminar for Friday December 2

Finally tagless, partially evaluated:

Tagless staged interpreters for simpler typed languages

Chung-chieh Shan (joint work with Jacques Carette and Oleg Kiselyov)

This "functional necklace" aims to change how you try to write your next interpreter: by deforesting the object language, to exhibit more static safety in a simpler type system.  We show how easy it is to build a family of interpreters for a typed object language (such as the simply typed lambda calculus) in a typed metalanguage (such as Haskell or ML) that preserve types without using dependent types, generalized algebraic data types, or postprocessing to eliminate tags.  The interpreters include an evaluator, a compiler, a partial evaluator, and call-by-name and call-by-value CPS transformers.

Our main idea is to encode abstract syntax using cogen functions rather than data constructors.  In other words, we represent object terms not in an initial algebra but in an arbitrary algebra.  Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformation.  Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.

This Friday’s seminar will take place in Upson 5126 from 12:05-1:00PM.

See you all on 12/2!

PRL Seminar for Nov 18, 2011

A Conversation with Moshe Vardi

Join in a discussion with Professor Moshe Vardi on the topic of Logic in Computer Science.

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

The PRL Seminar has been postponed for this week. We are planning a Seminar for next Friday (11/18) with more details to follow.

Presented at the November 4, 2011 PRL Seminar

Join us as we expand our discussion of 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 and how Event ML and Nuprl cooperate to produce correct-by-construction code.

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-1P