Abstract Predicates and Mutable ADTs in Hoare Type Theory

View/ Open
Metadata
Show full item recordCitation
Nanevski, 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.Abstract
Hoare 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.Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAACitable link to this page
http://nrs.harvard.edu/urn-3:HUL.InstRepos:25620475
Collections
- FAS Scholarly Articles [18172]
Contact administrator regarding this item (to report mistakes or request changes)