Zobrazeno 1 - 10
of 48
pro vyhledávání: '"Theory of computation → Proof theory"'
Publikováno v:
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy
This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::913b4fa960593c990e1ee32beab9f347
https://inria.hal.science/hal-04083002v1/document
https://inria.hal.science/hal-04083002v1/document
Autor:
Das, Anupam, Melgaard, Lukas
We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain "impredicative" theories; moreover, our cyclic systems naturally
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2d6e31b334de7a52d96609cb32717ae4
http://arxiv.org/abs/2306.08535
http://arxiv.org/abs/2306.08535
Publikováno v:
FSTTCS 2022-42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
FSTTCS 2022-42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2022, Chennai, India. pp.35:1--35:23, ⟨10.4230/LIPIcs.FSTTCS.2022.35⟩
FSTTCS 2022-42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2022, Chennai, India. pp.35:1--35:23, ⟨10.4230/LIPIcs.FSTTCS.2022.35⟩
The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formula
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::16de1d38ebbb5a6dae1e386be7718d27
https://hal.science/hal-04061582/document
https://hal.science/hal-04061582/document
Publikováno v:
31st EACSL Annual Conference on Computer Science Logic: CSL 2023, February 13-16, 2023, Warsaw, Poland
31st EACSL Annual Conference on Computer Science Logic
31st EACSL Annual Conference on Computer Science Logic
Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::98dc879a0ccd747f6dc03fd43d785820
https://hdl.handle.net/11245.1/9f9c4f06-1493-4444-bfbb-a7d6a6ea0a53
https://hdl.handle.net/11245.1/9f9c4f06-1493-4444-bfbb-a7d6a6ea0a53
Autor:
Barenbaum, Pablo, Freund, Teodoro
The λ^{PRK}-calculus is a typed λ-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend λ^{PRK} to encompass classical se
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e532a146990f61ce49d499fcfe3aa6cd
Autor:
Galmiche, Didier, Méry, Daniel
In this paper, we define the logic of Linear Temporal Bunched Implications (LTBI), a temporal extension of the Bunched Implications logic BI that deals with resource evolution over time, by combining the BI separation connectives and the LTL temporal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::64a91eb082b52afac33e6b0bb3845d5e
Autor:
Espírito Santo, José, Mendes, Filipa
The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lam
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::fd990a4c01525b0565a59b55b35156ec
Autor:
Miller, Dale, Wu, Jui-Hsuan
We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::db9648ea17dd77ed8177418b56351724
Autor:
Blot, Valentin
Publikováno v:
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. pp.32:1-32:16, ⟨10.4230/LIPIcs.FSCD.2023.32⟩
FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. pp.32:1-32:16, ⟨10.4230/LIPIcs.FSCD.2023.32⟩
We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an inte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b247ee46961692b4a45c2798ab8252e4
Autor:
Tanaka, Hiromi
We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazi\'c and Schmitz (2015), we show that the deducibility problem for full Lambek calculus
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2d23434899936304caef9ea47d8c06f7