Nuprl’s Inductive Logical Forms
- Presented at AI4FM, Edinburgh, UK, Sept 1, 2015.
- Unofficial PDF
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.