KnowledgeBase » 
PUBLICATION
» ID = 748
Nuprl’s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
2015
- Presented at AI4FM, Edinburgh, UK, Sept 1, 2015.
- Unofficial PDF
Abstract
For more than a decade, we have been working on specifying, verifying, and synthesizing asynchronous distributed protocols using the Nuprl proof assistant. Only recently we have been able to do so for complicated protocols such as Paxos. This has been made possible thanks to the level of abstraction of our speciï¬cation language called the Logic of Events (LoE). This paper discusses our main automation tool, namely our Inductive Logical Forms (ILFs), which are ï¬rst order formulas that characterize the responses of a system to events in terms of observations made at causally prior events.