Abstract Predicates and Mutable ADTs in Hoare Type Theory
MetadataShow full item record
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.
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.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:25620475
- FAS Scholarly Articles