From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus
Logic in Computer Science
2011-09-23 v1
Abstract
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.
Cite
@article{arxiv.1109.4817,
title = {From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus},
author = {Steffen van Bakel and Luca Cardelli and Maria Grazia Vigliotti},
journal= {arXiv preprint arXiv:1109.4817},
year = {2011}
}
Comments
International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008