A Curry-Howard Foundation for Functional Computation with Control

Abstract

We introduce the type theory λμv, a call-by-value variant of Parigot's λμ-calculus, as a Curry-Howard representation theory of classical propositional proofs. The associated rewrite system is Church-Rosser and strongly normalizing, and definitional equality of the type theory is consistent, compatible with cut, congruent and decidable. The attendant call-by-value programming language μPCFv is obtained from λμv by augmenting it by basic arithmetic, conditionals and fixpoints. We study the behavioural properties of μPCFv and show that, though simple, it is a very general language for functional computation with control: it can express all the main control constructs such as exceptions and first-class continuations. Proof-theoretically the dual λμv-constructs of naming and μ-abstraction witness the introduction and elimination rules of absurdity respectively. Computationally they give succinct expression to a kind of generic (forward) "jump" operator, which may be regarded as a unifying control construct for functional computation. Our goal is that λμv and μPCFv respectively should be to functional computation with first-class access to the flow of control what λ-calculus and PCF respectively are to pure functional programming: λμv gives the logical basis via the Curry-Howard correspondence, and μPCFv is a prototypical language albeit in purified form.