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

3Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

Abstract

We derive a Floyd-Hoare logic for non-local jumps and mutable higher-order procedural variables from a formulæ-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. © 2012 Elsevier Inc. All rights reserved.

Cite

CITATION STYLE

APA

Crolard, T., & Polonowski, E. (2012). Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control. In Journal of Logic and Algebraic Programming (Vol. 81, pp. 181–208). https://doi.org/10.1016/j.jlap.2012.01.004

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free