| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [18 references]
https://hal.inria.fr/hal-01091570
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, December 5, 2014 - 4:20:12 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Monday, March 9, 2015 - 6:04:43 AM
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, December 5, 2014 - 4:20:12 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Monday, March 9, 2015 - 6:04:43 AM
Files
eqfix-hal.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License