6 citations · 7 across the 7 of their papers we have counts for
7 papers
DBGen User Manual
Emmanuel Polonowski
DBGen is a tool for Coq developers. It takes as input the definition of a term structure with bindings annotations and generates definitions and properties for lifting and substitu…
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…
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…
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…
LoopW Technical Reference v0.3
Emmanuel Polonowski
This document describes the implementation in SML of the LoopW language, an imperative language with higher-order procedural variables and non-local jumps equiped with a program lo…
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Tristan Crolard, Emmanuel Polonowski
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…