Luca Cardelli, Steffen van Bakel, Maria Vigliotti
We study the π-calculus, enriched with pairing and non-blocking in-
put, and deﬁne 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 π.
Information from pubs.doc.ic.ac.uk/clac08.