Abstract Predicates And Mutable Adts In Hoare Type Theory
ESOP'07: Proceedings of the 16th European Symposium on Programming(2007)
摘要
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 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 that demand ownership of mutable memory, including an idealized custom memory manager.
更多查看译文
关键词
abstract predicate,abstract data type,Hoare Type Theory,higher-order language,higher-order logic,idealized custom memory manager,mutable memory,Extended Calculus,Hoare-like specification,Separation Logic,hoare type theory,mutable adts
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络