Affine Control Logic

This paper extends our previous work in combining classical logic with intuitionistic logic [LM13a, LM13b] to also include affine linear logic (linear logic with weakening), resulting in a unified system that we call Affine Control Logic. The goal is to allow affine-linear extensions of the Curry-Howard isomorphism to be combined with the well known capabilities of classical λµ calculus. To this end linear logic is adjusted so that contraction is not enabled by the exponential? but by a restricted form of Peirce’s formula. This formula also has a dual, which replaces the role of! in cut elimination. Classical fragments of proofs are better isolated from non-classical fragments, thus allowing different logics to coexist without a collapse. We define a phase space semantics for this logic and a sequent calculus that is proved to be sound and complete. A natural deduction system with a Curry-Howard interpretation is then defined. We demonstrate this system by showing how it can improve the formulation of exceptio