Source-linked AI summary
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
Tristan Crolard, Emmanuel Polonowski
TL;DR
Hoare-Floyd logic for non-local jumps lacks a straightforward derivation of the consequence rule because proof-obligation terms can interact with programs. The paper addresses this by distinguishing purely functional terms from imperative procedures, presenting a general solution to the problem.
Problem
Deriving Hoare-Floyd logic for non-local jumps is difficult because classical logic lacks an obvious data-mute notion, making the consequence rule generally underivable.
Method
The approach distinguishes purely functional terms from imperative procedures that may contain non-local jumps.
Results
The paper presents a general solution to deriving Hoare-Floyd logic for non-local jumps based on this distinction.
Takeaways & Limitations
Separating functional terms from imperative procedures addresses the interaction between proof-obligation terms and programs under control operators.
Abstract
from arXiv · showhide
We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formulæ-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.
Embedding a Hoare-Floyd logic
The logic embeds Hoare-Floyd reasoning in the imperative dependent type system by representing assertions with a global, state-passed variable. The consequence rule requires special treatment, but becomes derivable when assertions are restricted to data-mute formulas.
- Embedding a Hoare-Floyd logic: Hoare-Floyd triples are embedded using a global mutable variable `assert`, passed explicitly as an input and output parameter in procedure calls.Sequences receive sequents of the form Γ;Ω,assert : ϕ ⊢s ⊲Ω′,assert : ψ.
- Embedding a Hoare-Floyd logic: The consequence rule is the only Hoare-Floyd rule identified as not directly derivable.Its proof obligations require specific treatment because no proof-term is required for them.
- Embedding a Hoare-Floyd logic: Restricting assertions to data-mute formulas makes the consequence rule derivable without loss of generality.Data-mute proofs are described as having no computational content in intuitionistic logic.
Non-local jumps
This section extends the imperative language with labels and non-local jumps, corresponding at the dependent type level to classical logic. It highlights why deriving Hoare-Floyd logic is difficult and motivates a general solution to the failure of consequence-rule derivability.
- Language extension: Labels and non-local jumps extend the imperative language to IDc, whose dependent type system corresponds to classical logic with first-class labels typed by negation.The extension generalizes the underlying logic from intuitionistic to classical logic.
- Logical challenge: Hoare-Floyd logic is difficult to derive because classical logic lacks an obvious data-mute formula, so the consequence rule is generally not derivable.With control operators, proof terms associated with proof obligations can interact with the program.