From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus
arXiv:1109.4817
Abstract
We study the Pi-calculus, enriched with pairing and non-blocking input, and define a notion of type assignment that uses the type constructor "arrow". We encode the circuits of the calculus X into this variant of Pi, and show that all reduction (cut-elimination) and assignable types are preserved. Since X enjoys the Curry-Howard isomorphism for Gentzen's calculus LK, this implies that all proofs in LK have a representation in Pi.
International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008