Certified Web Services in Ynot

DSpace/Manakin Repository

Certified Web Services in Ynot

Citable link to this page


Title: Certified Web Services in Ynot
Author: Wisnesky, Ryan; Malecha, Gregory Michael; Morrisett, John Gregory

Note: Order does not necessarily reflect citation order of authors.

Citation: Wisnesky, Ryan, Gregory Malecha, and Greg Morrisett. 2009. Certified Web Services in Ynot. In Proceedings, 5th International Workshop on Automated Specification and Verification of Web Systems: July 17, 2009, Castle of Hagenberg, Austria.
Full Text & Related Files:
Abstract: In this paper we demonstrate that it is possible to implement certi ed web systems in a way not much di erent from writing
Standard ML or Haskell code, including use of imperative features like pointers, les, and socket I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certi ed imperative programming.We add a dialog-based I/O system to Ynot, and we extend Ynot's underlying Hoare logic with event traces to reason about I/O be- havior. Expressive abstractions allow the modular certi cation of both high level speci cations like privacy guarantees and low level properties like memory safety and correct parsing.
Published Version: http://www.risc.uni-linz.ac.at/about/conferences/wwv09/
Other Sources: http://ynot.cs.harvard.edu/papers/wwv09.pdf
Terms of Use: This article is made available under the terms and conditions applicable to Open Access Policy Articles, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#OAP
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980868
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search