Zobrazeno 1 - 10
of 6 519
pro vyhledávání: '"[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]"'
Autor:
Bruno Courcelle
Publikováno v:
Discrete Mathematics & Theoretical Computer Science, Vol vol. 23 no. 2, special issue..., Iss Special issues (2022)
The ternary relation B(x,y,z) of betweenness states that an element y is between the elements x and z, in some sense depending on the considered structure. In a partially ordered set (N,≤), B(x,y,z):⇔x
Externí odkaz:
https://doaj.org/article/7d85493aec46492c9b2ae1b0e9ca647e
Autor:
Loïc Pujet, Nicolas Tabareau
Publikováno v:
POPL 2023 Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. pp.74, ⟨10.1145/3571739⟩
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. pp.74, ⟨10.1145/3571739⟩
International audience; In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::47771d66871d869f03c33deb8b658c38
https://doi.org/10.1145/3571739
https://doi.org/10.1145/3571739
Autor:
Paweł Parys
Publikováno v:
Discrete Mathematics & Theoretical Computer Science, Vol vol. 22 no. 4, Iss Automata, Logic and Semantics (2020)
We consider nondeterministic higher-order recursion schemes as recognizers of languages of finite words or finite trees. We propose a type system that allows to solve the simultaneous-unboundedness problem (SUP) for schemes, which asks, given a set o
Externí odkaz:
https://doaj.org/article/80aec6a61b1b432695b73a279022ee67
Autor:
Guardia, Rémi, Laurent, Olivier
Publikováno v:
Leibniz International Proceedings in Informatics (LIPIcs)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. pp.2, ⟨10.4230/LIPIcs.FSCD.2023.26⟩
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. ⟨10.4230/LIPIcs.FSCD.2023.22⟩
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. pp.2, ⟨10.4230/LIPIcs.FSCD.2023.26⟩
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. ⟨10.4230/LIPIcs.FSCD.2023.22⟩
We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::011c9e45ade7a3d0b39903a773340938
https://hal.science/hal-04082204v2/document
https://hal.science/hal-04082204v2/document
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
Publikováno v:
50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)
50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), Jul 2023, Paderborn, Germany. pp.120:1--120:17, ⟨10.4230/LIPIcs.ICALP.2023.120⟩
50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), Jul 2023, Paderborn, Germany. pp.120:1--120:17, ⟨10.4230/LIPIcs.ICALP.2023.120⟩
International audience; We exhibit a strong connection between the matchgate formalism introduced by Valiant and the ZW-calculus of Coecke and Kissinger. This connection provides a natural compositional framework for matchgate theory as well as a dir
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2028b7ad1a17b7ae750c037766b92520
https://hal.science/hal-04002282/document
https://hal.science/hal-04002282/document
Autor:
Dowek, Gilles
The set of pure terms which are typable in the $\lambda$$\Pi$-calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be mentioned
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6edc3ac2286d50983862f9ff5a189dc3
http://arxiv.org/abs/2306.07599
http://arxiv.org/abs/2306.07599
Big data programming frameworks have become increasingly important for the development of applications for which performance and scalability are critical. In those complex frameworks, optimizing code by hand is hard and time-consuming, making automat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2c8daa25a03aca01ba0ea09aa4c12fda
http://arxiv.org/abs/2306.07690
http://arxiv.org/abs/2306.07690
Autor:
Gilles Dowek
Publikováno v:
LICS
Scopus-Elsevier
Scopus-Elsevier
The problem of determining whether a term is an instance of another in the simply typed lambda -calculus, i.e. of solving the equation a=b where a and b are simply typed lambda -terms and b is ground, is addressed. An algorithm that decides whether a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::862d43a6dc44ce3e7181a9bac279457d
http://arxiv.org/abs/2306.01473
http://arxiv.org/abs/2306.01473
Autor:
Dowek, Gilles
Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8738fe16d4973a27ec0a041118c63ddb
http://arxiv.org/abs/2306.00495
http://arxiv.org/abs/2306.00495