Show simple item record

dc.contributor.authorWisnesky, Ryan
dc.contributor.authorMalecha, Gregory Michael
dc.contributor.authorMorrisett, John Gregory
dc.date.accessioned2010-04-21T14:44:34Z
dc.date.issued2010-04-21
dc.identifier.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.en_US
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:3980868
dc.description.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.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dc.relation.isversionofhttp://www.risc.uni-linz.ac.at/about/conferences/wwv09/en_US
dc.relation.hasversionhttp://ynot.cs.harvard.edu/papers/wwv09.pdfen_US
dash.licenseOAP
dc.titleCertified Web Services in Ynoten_US
dc.typeConference Paperen_US
dc.description.versionAccepted Manuscripten_US
dash.depositing.authorMorrisett, John Gregory
dc.date.available2010-04-21T14:44:34Z
dash.contributor.affiliatedWisnesky, Ryan
dash.contributor.affiliatedMalecha, Gregory Michael
dash.contributor.affiliatedMorrisett, Greg Gregory
dc.identifier.orcid0000-0003-3952-0807


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record