This month's Logical Methods in Computer Science (Vol 7 Issue 2) published an article by the PRL Group. The article Knowledge-Based Synthesis of Distributed Systems Using Event Structures by Mark Bickford, Robert Constable, Joseph Halpern, and Sabina Petride discusses... well rather than try to summarize it, here is the link and abstract:
Link: http://www.lmcs-online.org/ojs/viewarticle.php?id=496&layout=abstract
Abstract
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.