Classical Proofs, Typed Processes, and Intersection Types

Abstract

Curien and Herbelin provided a Curry and Howard correspondence between classical propositional logic and a computational model called $\overline{\lambda}\mu\widetilde{\mu}$ which is a calculus for interpreting classical sequents. A new terminology for $\overline{\lambda}\mu\widetilde{\mu}$ in terms of pairs of callers–callees which we name capsules enlightens a natural link between $\overline{\lambda}\mu\widetilde{\mu}$ and process calculi. In this paper we propose an intersection type system $\overline{\lambda}\mu\widetilde{\mu}^\cap$ which is an extension of $\overline{\lambda}\mu\widetilde{\mu}$ with intersection types. We prove that all strongly normalizing $\overline{\lambda}\mu\widetilde{\mu}$-terms are typeable in the new system, which was not the case in $\overline{\lambda}\mu\widetilde{\mu}$. Also, we prove that all typeable $\widetilde{\mu}$-free terms are strongly normalizing.