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...
| Main Authors: | , , |
|---|---|
| Format: | Text |
| Language: | unknown |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://arxiv.org/abs/1109.4817 |
| _version_ | 1821552125330587648 |
|---|---|
| author | van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia |
| author_facet | van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia |
| author_sort | van Bakel, Steffen |
| collection | ArXiv.org (Cornell University Library) |
| description | 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 |
| format | Text |
| genre | Iceland |
| genre_facet | Iceland |
| id | ftarxivpreprints:oai:arXiv.org:1109.4817 |
| institution | Open Polar |
| language | unknown |
| op_collection_id | ftarxivpreprints |
| op_relation | http://arxiv.org/abs/1109.4817 |
| publishDate | 2011 |
| record_format | openpolar |
| spelling | ftarxivpreprints:oai:arXiv.org:1109.4817 2025-01-16T22:35:20+00:00 From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia 2011-09-22 http://arxiv.org/abs/1109.4817 unknown http://arxiv.org/abs/1109.4817 Computer Science - Logic in Computer Science text 2011 ftarxivpreprints 2023-08-16T12:33:34Z 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 Text Iceland ArXiv.org (Cornell University Library) |
| spellingShingle | Computer Science - Logic in Computer Science van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title | From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title_full | From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title_fullStr | From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title_full_unstemmed | From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title_short | From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| title_sort | from x to pi; representing the classical sequent calculus in the pi-calculus |
| topic | Computer Science - Logic in Computer Science |
| topic_facet | Computer Science - Logic in Computer Science |
| url | http://arxiv.org/abs/1109.4817 |