AESOP home


From X to Pi: Representing Classical Sequent Calculus in Pi-calculus

Luca Cardelli, Steffen van Bakel, Maria Vigliotti

Conference or Workshop Paper
International Workshop on Classical Logic and Computation (CL&C'08)

We study the π-calculus, enriched with pairing and non-blocking in-

put, and define a notion of type assignment that uses the type constructor →. We

encode the circuits of the calculus X into this variant of π, and show that all

reduction (cut-elimination) and assignable types are preserved. Since X enjoys

the Curry-Howard isomorphism for Gentzen's calculus L K, this implies that all

proofs in L K have a representation in π.

PDF of full publication (171.6 kilobytes)
(need help viewing PDF files?)

Information from