Show simple item record

dc.contributor.authorNanevski, Aleksandar
dc.contributor.authorMorrisett, John Gregory
dc.contributor.authorShinnar, Avraham Ever
dc.contributor.authorGovereau, Paul
dc.contributor.authorBirkedal, Lars
dc.date.accessioned2010-04-21T14:42:47Z
dc.date.issued2008
dc.identifier.citationNanevski, Aleksandar, Greg Morrisett, Avi Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent types for imperative programs. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming: September 20-28, 2008, Victoria, BC, Canada, ed. J. Hook, 229-240. New York, N.Y.: ACM Press.en_US
dc.identifier.isbn978-1-59593-919-7en_US
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:3980866
dc.description.abstractWe describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dc.publisherAssociation for Computing Machineryen_US
dc.relation.isversionofhttp://portal.acm.org/citation.cfm?id=1411204.1411237en_US
dc.relation.hasversionhttp://ynot.cs.harvard.edu/papers/ynot08.pdfen_US
dash.licenseMETA_ONLY
dc.subjectType Theoryen_US
dc.subjectHoare Logicen_US
dc.subjectSeparation Logicen_US
dc.subjectMonadsen_US
dc.titleYnot: Dependent Types for Imperative Programsen_US
dc.typeConference Paperen_US
dc.description.versionAuthor's Originalen_US
dash.depositing.authorMorrisett, John Gregory
dash.embargo.until10000-01-01
dc.identifier.doi10.1145/1411203.1411237
dash.contributor.affiliatedShinnar, Avraham Ever
dash.contributor.affiliatedGovereau, Paul
dash.contributor.affiliatedMorrisett, Greg Gregory


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record