Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LPAR

2004

Springer

2004

Springer

Abstract. To produce a program guaranteed to satisfy a given speciﬁcation one can synthesize it from a formal constructive proof that a computation satisfying that speciﬁcation exists. This process is particularly eﬀective if the speciﬁcations are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level speciﬁcation language that results from adding knowledge to a fragment of Nuprl speciﬁcally tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based speciﬁcations using a proof development system such as Nuprl. Methods of Halpern and Zuck [15] then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.

Related Content

Added |
02 Jul 2010 |

Updated |
02 Jul 2010 |

Type |
Conference |

Year |
2004 |

Where |
LPAR |

Authors |
Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride |

Comments (0)