Equality and fixpoints in the calculus of structures

Kaustuv Chaudhuri; Nicolas Guenot

doi:10.1145/2603088.2603140

Equality and fixpoints in the calculus of structures

Kaustuv Chaudhuri, Nicolas Guenot

Programming Logic and Semantics

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

Abstract

The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic.
This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.

Originalsprog	Engelsk
Titel	Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014
Redaktører	Thomas A. Henzinger, Dale Miller
Antal sider	10
Forlag	Association for Computing Machinery
Publikationsdato	12 sep. 2014
Sider	30-40
ISBN (Trykt)	978-1-4503-2886-9
DOI	https://doi.org/10.1145/2603088.2603140
Status	Udgivet - 12 sep. 2014

Navn	Annual Symposium on Logic in Computer Science
ISSN	1043-6871

Emneord

Deep inference
Unification
Fixed points
Linear logic

Adgang til dokumentet

10.1145/2603088.2603140

http://doi.acm.org/10.1145/2603088.2603140

Citationsformater

Chaudhuri, K., & Guenot, N. (2014). Equality and fixpoints in the calculus of structures. I T. A. Henzinger, & D. Miller (red.), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014 (s. 30-40). Association for Computing Machinery. https://doi.org/10.1145/2603088.2603140

Chaudhuri, Kaustuv ; Guenot, Nicolas. / Equality and fixpoints in the calculus of structures. Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. red. / Thomas A. Henzinger ; Dale Miller. Association for Computing Machinery, 2014. s. 30-40 (Annual Symposium on Logic in Computer Science).

@inproceedings{9e76d1dd1cde4fe7a7b53082d90db992,

title = "Equality and fixpoints in the calculus of structures",

abstract = "The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic.This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.",

keywords = "Deep inference, Unification, Fixed points, Linear logic, Deep inference, Unification, Fixed points, Linear logic",

author = "Kaustuv Chaudhuri and Nicolas Guenot",

year = "2014",

month = sep,

day = "12",

doi = "10.1145/2603088.2603140",

language = "English",

isbn = "978-1-4503-2886-9",

series = "Annual Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

pages = "30--40",

editor = "Henzinger, {Thomas A.} and Dale Miller",

booktitle = "Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014",

address = "United States",

}

Chaudhuri, K & Guenot, N 2014, Equality and fixpoints in the calculus of structures. i TA Henzinger & D Miller (red), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. Association for Computing Machinery, Annual Symposium on Logic in Computer Science, s. 30-40. https://doi.org/10.1145/2603088.2603140

Equality and fixpoints in the calculus of structures. / Chaudhuri, Kaustuv; Guenot, Nicolas.
Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. red. / Thomas A. Henzinger; Dale Miller. Association for Computing Machinery, 2014. s. 30-40 (Annual Symposium on Logic in Computer Science).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Equality and fixpoints in the calculus of structures

AU - Chaudhuri, Kaustuv

AU - Guenot, Nicolas

PY - 2014/9/12

Y1 - 2014/9/12

N2 - The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic.This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.

AB - The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic.This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.

KW - Deep inference

KW - Unification

KW - Fixed points

KW - Linear logic

KW - Deep inference

KW - Unification

KW - Fixed points

KW - Linear logic

U2 - 10.1145/2603088.2603140

DO - 10.1145/2603088.2603140

M3 - Article in proceedings

SN - 978-1-4503-2886-9

T3 - Annual Symposium on Logic in Computer Science

SP - 30

EP - 40

BT - Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014

A2 - Henzinger, Thomas A.

A2 - Miller, Dale

PB - Association for Computing Machinery

ER -

Chaudhuri K, Guenot N. Equality and fixpoints in the calculus of structures. I Henzinger TA, Miller D, red., Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. Association for Computing Machinery. 2014. s. 30-40. (Annual Symposium on Logic in Computer Science). doi: 10.1145/2603088.2603140

Equality and fixpoints in the calculus of structures

Abstract

Emneord

Adgang til dokumentet

Fingeraftryk

Citationsformater