Ynot: Dependent Types for Imperative Programs

DSpace/Manakin Repository

Ynot: Dependent Types for Imperative Programs

Show simple item record

dc.contributor.author Nanevski, Aleksandar
dc.contributor.author Morrisett, John Gregory
dc.contributor.author Shinnar, Avraham Ever
dc.contributor.author Govereau, Paul
dc.contributor.author Birkedal, Lars
dc.date.accessioned 2010-04-21T14:42:47Z
dc.date.issued 2008
dc.identifier.citation Nanevski, 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.isbn 978-1-59593-919-7 en_US
dc.identifier.uri http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980866
dc.description.abstract We 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.sponsorship Engineering and Applied Sciences en_US
dc.language.iso en_US en_US
dc.publisher Association for Computing Machinery en_US
dc.relation.isversionof http://portal.acm.org/citation.cfm?id=1411204.1411237 en_US
dc.relation.hasversion http://ynot.cs.harvard.edu/papers/ynot08.pdf en_US
dash.license META_ONLY
dc.subject Type Theory en_US
dc.subject Hoare Logic en_US
dc.subject Separation Logic en_US
dc.subject Monads en_US
dc.title Ynot: Dependent Types for Imperative Programs en_US
dc.type Conference Paper en_US
dc.description.version Author's Original en_US
dash.depositing.author Morrisett, John Gregory
dash.embargo.until 10000-01-01

Files in this item

Files Size Format View xmlui.dri2xhtml.METS-1.0.item-files-description
Nanevski_Ynot.pdf 272.7Kb PDF View/Open Title has changed in the published versrion.

This item appears in the following Collection(s)

  • FAS Scholarly Articles [6948]
    Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University

Show simple item record

 
 

Search DASH


Advanced Search
 
 

Submitters