@inproceedings{02666f6b50a7428f9c6caac3e46bfc3c,
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, Fixed Points, Linear Logic, Unification",
author = "Kaustuv Chaudhuri and Nicolas Guenot",
year = "2014",
month = jan,
day = "1",
doi = "10.1145/2603088.2603140",
language = "English",
isbn = "9781450328869",
series = "Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014",
publisher = "Association for Computing Machinery",
booktitle = "Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014",
note = "Joint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 ; Conference date: 14-07-2014 Through 18-07-2014",
}