Ynot: dependent types for imperative programs
Ynot: dependent types for imperative programs
复制标题
DOI：
10.1145/1411204.1411237
复制
发表时间：
2008-09
期刊：
影响因子：
--
通讯作者：
Aleksandar Nanevski;Greg Morrisett;Avraham Shinnar;Paul Govereau;L. Birkedal
中科院分区：
文献类型：
--
作者：
Aleksandar Nanevski;Greg Morrisett;Avraham Shinnar;Paul Govereau;L. Birkedal
我们描述了Coq证明助手的一个公理扩展，它支持编写、推理和提取具有副作用的高阶、依赖类型的程序。Coq已经包含了一种强大的支持依赖类型的函数式语言，但是这种语言仅限于纯函数。我们的扩展（我们称之为Ynot）的主要贡献是增加了对计算的支持，这些计算可能具有诸如不终止、访问可变存储以及抛出/捕获异常等效果。Ynot公理形成了一个小型的可信计算基础，在我们之前关于Hoare类型理论（HTT）的工作中已经正式证明了这一点。我们将展示如何将这些公理与Coq强大的类型和抽象机制结合起来，以构建更高级的推理机制，而这些推理机制又可用于构建实际的、经过验证的软件组件。为了证实这一说法，我们在这里描述了一系列实现命令式有限映射的代表性模块，包括对高阶（有效）迭代器的支持。实现范围从简单（如关联列表）到复杂（如哈希表），但共享一个抽象实现细节的公共接口，并确保模块正确实现有限映射抽象。
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 higher-order (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.