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

DOI10.1016/J.JLAP.2012.01.004MaRDI QIDQ444460zbMATH OpenOpenAlexFDO

Publication date 14 August 2012

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1112.2950

continuation monad Floyd-Hoare logic callcc higher-order procedure imperative dependent type system for Hoare triples non-local jumps

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formul{ae}-as-types notion of control for classical logic. The main contribution of this work is the design of an imperative dependent type system for non-local jumps which corresponds to classical logic but where the famous consequence rule is still derivable.

Recommendations

Cites work

Cited in

(2)

Describes a project that uses

Uses Software

This page was built for publication: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q444460)