A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps

TL;DR

This paper develops a formal program logic for higher-order procedural variables and non-local jumps, utilizing Ott and Twelf, with executable specifications and verified examples demonstrating correctness.

Contribution

It introduces a formal logic for complex control flow features, with executable specifications and mechanically verified correctness using Twelf.

Findings

Successfully specified a logic for higher-order procedures and jumps

Mechanically verified correctness of example programs

Provided executable specifications in Twelf

Abstract

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 both executable specifications thanks to Twelf's logic programming engine. In particular, relying on Filinski's encoding of shift/reset using callcc/throw and a global meta-continuation (simulated in state passing style), we have mechanically checked the correctness of a few examples (all source files are available on request).