EventML is a functional programming language in the ML family, closely related to Classic ML GMW79, CHP84, KR11]. 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) Bic09, BC08], hence the name “EventML”. The Event Logic combinators are high level specifications of distributed computations whose properties can be naturally expressed in Event Logic. The combinators can be formally translated (compiled) into the process model underlying Event Logic and thus converted to distributed programs. The interactions of these high level distributed programs manifest the behavior described by the logic. EventML can thus both specify and execute the processes that create the behaviors, called event structures, arising from the interactions of the processes.
Since EventML can directly specify computing tasks using the event combinators it can carry out part of the task normally assigned to a theorem prover, formal specification. EventML can also interact with a theorem prover, presently Nuprl CAB+86, Kre02, ABC+06] (a theorem prover based on a constructive type theory called Computational Type Theory (CTT) CAB+86] and on Classic ML), which can express logical properties and constraints on the evolving computations as formulas of Event Logic and prove them. From these proofs, a prover can create correct-by-construction process terms which EventML can execute. Thus EventML and Nuprl can work together synergistically in creating a correct by construction concurrent system. EventML could play the same role with respect to any theorem prover that implements the Logic of Events. Thus EventML provides a new paradigm for creating correct distributed systems, one in which a systems programmer can design and code a system using event combinators in such a way that a theorem prover can easily express and prove logical properties of the resulting computations. To EventML, the event combinators have a dual character. They have the logical character of specifications and the computational character of producing event structures with formally guaranteed behaviors.
EventML was created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE) ABC+06].
In one direction, EventML can import logical specifications from the prover as well as event class specifications and the process code that realizes them. In the present mode of operation, EventML docks with the Nuprl prover to obtain this information.
In the other direction, EventML can be used by programmers to specify protocols using event logic combinators. Following the line of work in which Nuprl was used to reason about the Ensemble system Hay98, BCH+00, KHH98, LKvR+99] (coded in OCaml Ler00]), EventML, by docking to Nuprl, provides a way to reason about (and synthesize) many distributed protocols. Thanks to its constructive logic, its expressiveness, and its large library, Nuprl is well suited to reason about distributed systems BKR01]. But in principle EventML can connect to any prover that implements Event Logic and our General Process Model BCG10]. Given an EventML specification, the Nuprl prover can: (1) synthesize process code, and (2) generate the inductive logical form of the specification which is used to structure logical description of the protocols and the system.
