6 citations · 7 across the 7 of their papers we have counts for
Showing 2011Show all
3 papers · 1 filter
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★ 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…
cs.LO2011★ 1 cited
Generic Environments in Coq
Emmanuel Polonowski
We introduce a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for…