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: Text
Language:unknown
Published: 2011
Subjects:
Computer Science - Logic in Computer Science
Iceland
Online Access:http://arxiv.org/abs/1109.4817
id ftarxivpreprints:oai:arXiv.org:1109.4817
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:1109.4817 2023-09-05T13:20:29+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 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)
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Computer Science - Logic in Computer Science
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
topic_facet Computer Science - Logic in Computer Science
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_relation http://arxiv.org/abs/1109.4817
_version_ 1776201166982479872

Similar Items