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

TL;DR

This paper develops a Hoare-Floyd logic for non-local jumps using a formul{ ae}-as-types approach, creating an imperative dependent type system aligned with classical logic that retains the consequence rule.

Contribution

It introduces a novel imperative dependent type system for non-local jumps derived from a formul{ ae}-as-types framework, bridging classical logic and control flow reasoning.

Findings

A new Hoare-Floyd logic for non-local jumps is formulated.

The type system supports classical logic with a derivable consequence rule.

The approach connects control flow and dependent types in imperative programming.

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.