From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus

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 pr...

Full description

Bibliographic Details
Main Authors: van Bakel, Steffen, Cardelli, Luca, Vigliotti, Maria Grazia
Format: Text
Language:unknown
Published: 2011
Subjects:
Computer Science - Logic in Computer Science
Iceland
Online Access:http://arxiv.org/abs/1109.4817
Description
Summary: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. Comment: International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008

Similar Items