A program logic for higher-order procedural variables and non-local jumps
Logic in Computer Science
2015-03-19 v1
Abstract
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, we show how to derive a sound program logic for this programming language. As a by-product, we obtain a non-dependent type system which is more permissive than what is usually found in statically typed imperative languages. As a generic example, we encode imperative versions of delimited continuations operators shift and reset.
Cite
@article{arxiv.1112.1554,
title = {A program logic for higher-order procedural variables and non-local jumps},
author = {Tristan Crolard and Emmanuel Polonowski},
journal= {arXiv preprint arXiv:1112.1554},
year = {2015}
}