Wisnesky, RyanMalecha, Gregory MichaelMorrisett, Greg Gregory2010-04-212010-04-21Wisnesky, 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.http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980868In 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.en-USConference Paper2010-04-21