The series of workshops on Intuitionistic Modal Logic and Applications (IMLA) owes its existence to the hope that philosophers, mathematical logicians and computer scientists would share information and tools when investigating intuitionistic modal logics and modal type theories, if they knew of each other's work. More than 10 years have passed since the retrospective view of de Paiva et al. [ 10 ], and progress in the area of constructive modal logic has been slow and getting slower. It is our view that differences in the outlook of the various groups of scholars interested in the topic, differences that were once fruitful, now are responsible for a tendency for the new work to be driven by technical issues that have not had wide interest, leading to compartmentalization and waning interest in the IMLA big tent. Work on modal type theories seems to have been pursued in narrow tracts. For instance, much work in the symposium on Principles of Programming Languages (POPL), in specific type systems could be considered work in applied constructive modal logic, but it is not considered so, as this perspective is not considered useful or productive. Generally speaking, topic specialists have stopped expecting outsiders to say anything of interest to them, so they do not make the effort to say anything of interest to outsiders.

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.