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

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

2011-09-22

arxiv.org/abs/1109.4817v1

Computer Science

Logic in Computer Science

International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-263155