Intuitionistic Letcc via Labelled Deduction

The well-known embedding of intuitionistic logic into classical modal logic means that intuitionistic logic can be viewed as a calculus of labelled deduction on multiple-conclusion sequents, where the labels are the Kripke worlds of the modal embedding. The corresponding natural deduction system constitutes a type system for programs using control operators such as letcc that capture the current program continuation, which has a modal restriction on the use of such continuations that enforces constructive validity. This allows us to develop a rich dependent type theory incorporating letcc, which is known to be otherwise highly problematic for computational interpretations of classical logic. Moreover, we give a novel constructive proof for the soundness of this labelled deduction system, whose algorithmic content is a non-deterministic translation of programs that eliminates uses of letcc and is fully compatible with dependent types and therefore with program verification. This proof has been formally verified on the propositional fragment in the Twelf meta-logical framework.