Deriving a Floyd-Hoare logic for non-local jumps from a formulae-as-types notion of control

被引：2

作者：

Crolard, T. ^{[1
]}

Polonowski, E. ^{[1
]}

机构：

[1] Univ Paris Est, LACL, F-94010 Creteil, France

来源：

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2012年 / 81卷 / 03期

关键词：

Floyd-Hoare logic; Higher-order procedure; jump; callcc; Continuation; Monad; PROGRAM EXTRACTION; ALGOL; 60; LANGUAGE;

D O I：

10.1016/j.jlap.2012.01.004

中图分类号：

学科分类号：

摘要：

We derive a Floyd-Hoare logic for non-local jumps and mutable higher-order procedural variables from a formula-as-types notion of control for classical logic. A key contribution of this work is the design of an imperative dependent type system for Hoare triples, which corresponds to classical logic, but where the famous consequence rule is admissible. Moreover, we prove that this system is complete for a reasonable notion of validity for Hoare judgments. (C) 2012 Elsevier Inc. All rights reserved.

引用

页码：181 / 208

页数：28