Certified Web Services in Ynot
MetadataShow full item record
CitationWisnesky, 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.
AbstractIn 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.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:3980868
- FAS Scholarly Articles