We study the π-calculus, enriched with pairing, and define a notion of type assignment that uses the type constructor →. We define a calculus LK, a variant of the calculus X that allows arbitrary progress of cut over cut, and interpret its terms into this variant of π, and show that all reduction and assignable types are preserved. Since LK enjoys the Curry-Howard isomorphism for Gentzen's calculus LK, this implies that all proofs in LK have a representation in π, and cut-elimination is simulated by π's synchronisation and congruence of processes. We then enrich the logic with the connector ¬, and show that this also can be represented in π.
