Show simple item record

dc.contributor.authorNanevski, Aleksandar
dc.contributor.authorAhmed, Amal
dc.contributor.authorMorrisett, Greg Gregory
dc.contributor.authorBirkedal, Lars
dc.date.accessioned2016-02-25T17:38:18Z
dc.date.issued2006
dc.identifier.citationNanevski, Aleksandar, Amal Ahmed, Greg Morrisett, and Lars Birkedal. 2006. Abstract Predicates and Mutable ADTs in Hoare Type Theory. Harvard Computer Science Group Technical Report TR-14-06.en_US
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:25620475
dc.description.abstractHoare Type Theory (HTT) combines a dependently typed, higher-order language with monadically-encapsulated, stateful computations. The type system incorporates pre- and post-conditions, in a fashion similar to Hoare and Separation Logic, so that programmers can modularly specify the requirements and effects of computations within types. This paper extends HTT with quantification over abstract predicates (i.e., higher-order logic), thus embedding into HTT the Extended Calculus of Constructions. When combined with the Hoare-like specifications, abstract predicates provide a powerful way to define and encapsulate the invariants of private state; that is, state which may be shared by several functions, but is not accessible to their clients. We demonstrate this power by sketching a number of abstract data types and functions that demand ownership of mutable memory, including an idealized custom memory manager.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dash.licenseLAA
dc.titleAbstract Predicates and Mutable ADTs in Hoare Type Theoryen_US
dc.typeResearch Paper or Reporten_US
dc.description.versionVersion of Recorden_US
dash.depositing.authorMorrisett, Greg Gregory
dc.date.available2016-02-25T17:38:18Z
dash.contributor.affiliatedMorrisett, Greg Gregory


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record