Ynot: Depent Types for Imperative Programs

Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    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 higherorder (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.
    Original languageEnglish
    Title of host publicationInternational Conference on Functional Programming : Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,
    Volumesession 9
    PublisherAssociation for Computing Machinery
    Publication date2008
    Pages229-240
    ISBN (Print)978-1-59593-919-7
    Publication statusPublished - 2008
    EventICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming - Victoria, British Columbia, Canada
    Duration: 22 Sep 200824 Sep 2008
    Conference number: 13

    Conference

    ConferenceICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming
    Number13
    Country/TerritoryCanada
    CityVictoria, British Columbia
    Period22/09/200824/09/2008

    Cite this