6 citations · 9 across the 6 of their papers we have counts for
Showing 2011 · cs.LOShow all
3 papers · 2 filters
cs.LO2011
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
Tristan Crolard, Emmanuel Polonowski
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…
cs.LO2011★ 2 cited
A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps
Tristan Crolard
We formally specified a program logic for higher-order procedural variables and non-local jumps with Ott and Twelf. Moreover, the dependent type systems and the translation are bot…
cs.LO2011★ 6 cited
A program logic for higher-order procedural variables and non-local jumps
Tristan Crolard, Emmanuel Polonowski
Relying on the formulae-as-types paradigm for classical logic, we define a program logic for an imperative language with higher-order procedural variables and non-local jumps. Then…