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: Report
Language:unknown
Published: arXiv 2011
Subjects:
Logic in Computer Science cs.LO
FOS Computer and information sciences
Iceland
Online Access:https://dx.doi.org/10.48550/arxiv.1109.4817
https://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. : International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008

Similar Items