Equality and fixpoints in the calculus of structures

Kaustuv Chaudhuri, Nicolas Guenot

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-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.
Original languageEnglish
Title of host publicationJoint 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
EditorsThomas A. Henzinger, Dale Miller
Number of pages10
PublisherAssociation for Computing Machinery
Publication date12 Sept 2014
Pages30-40
ISBN (Print)978-1-4503-2886-9
DOIs
Publication statusPublished - 12 Sept 2014
SeriesAnnual Symposium on Logic in Computer Science
ISSN1043-6871

Keywords

  • Deep inference
  • Unification
  • Fixed points
  • Linear logic

Fingerprint

Dive into the research topics of 'Equality and fixpoints in the calculus of structures'. Together they form a unique fingerprint.

Cite this