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: | English |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://arxiv.org/abs/1109.4817 |
| id |
fttriple:oai:gotriple.eu:10670/1.sq7gd0 |
|---|---|
| record_format |
openpolar |
| spelling |
fttriple:oai:gotriple.eu:10670/1.sq7gd0 2023-05-15T16:48:06+02: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 en eng 10670/1.sq7gd0 http://arxiv.org/abs/1109.4817 undefined arXiv phil lang Text https://vocabularies.coar-repositories.org/resource_types/c_18cf/ 2011 fttriple 2023-01-22T17:26:10Z 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 Unknown |
| institution |
Open Polar |
| collection |
Unknown |
| op_collection_id |
fttriple |
| language |
English |
| topic |
phil lang |
| spellingShingle |
phil lang van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus |
| topic_facet |
phil lang |
| 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 |
| author |
van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia |
| author_facet |
van Bakel, Steffen Cardelli, Luca Vigliotti, Maria Grazia |
| author_sort |
van Bakel, Steffen |
| title |
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_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_sort |
from x to pi; representing the classical sequent calculus in the pi-calculus |
| publishDate |
2011 |
| url |
http://arxiv.org/abs/1109.4817 |
| genre |
Iceland |
| genre_facet |
Iceland |
| op_source |
arXiv |
| op_relation |
10670/1.sq7gd0 http://arxiv.org/abs/1109.4817 |
| op_rights |
undefined |
| _version_ |
1766038220943917056 |