Introduction to EventML, version 0.2

Mark Bickford, Robert L. Constable, Richard Eaton,
David Guaspari, and Vincent Rahli

March 2, 2012

EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name “EventML”. more about specifications »

EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE). more about theorem prover interface »

This tutorial also includes multiple example protocols, including:

To download EventML and for additional documentation see: http://www.nuprl.org/software

About this document
This is a web projection of An Introduction to Event ML [PDF] created Feb. 2012 using tex4ht.

EventML docks with Nuprl
EventML

Contents
1 Introduction
 1.1 Specification and Programming
 1.2 Interaction with theorem provers
2 Event Logic
 2.1 Events, event orderings, and event classes
 2.2 Inductive logical forms
3 Simple examples
 3.1 Ping-pong
 3.2 Ping-pong with memory
 3.3 Leader election in a ring
4 State machines
 4.1 Moore machines, “pre” and “post”
 4.2 Moore machines with multiple transition functions
5 The two-thirds consensus protocol
 5.1 The specification of 2/3-consensus
 5.2 Illustrative runs of the protocol
 5.3 Properties of the 2/3-consensus protocol
6 Paxos
7 Definitions of combinators
8 Configuration files
9 EventML’s syntax
References
Index