Logical Methods in Computer Science - Latest Publications Latest papers https://lmcs.episciences.org/img/episciences_sign_50x50.png episciences.org https://lmcs.episciences.org Wed, 28 Sep 2022 20:06:23 +0000 episciences.org https://lmcs.episciences.org Logical Methods in Computer Science Logical Methods in Computer Science A categorical framework for congruence of applicative bisimilarity in higher-order languages Wed, 21 Sep 2022 05:20:34 +0000 https://doi.org/10.46298/lmcs-18(3:37)2022 https://doi.org/10.46298/lmcs-18(3:37)2022 Hirschowitz, Tom Lafont, Ambroise Hirschowitz, Tom Lafont, Ambroise 0 On sets of terms having a given intersection type Wed, 21 Sep 2022 05:18:05 +0000 https://doi.org/10.46298/lmcs-18(3:35)2022 https://doi.org/10.46298/lmcs-18(3:35)2022 Polonsky, Andrew Statman, Richard Polonsky, Andrew Statman, Richard 0 A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods Wed, 21 Sep 2022 05:13:51 +0000 https://doi.org/10.46298/lmcs-18(3:36)2022 https://doi.org/10.46298/lmcs-18(3:36)2022 Ikebuchi, Mirai Ikebuchi, Mirai 0 Relating Functional and Imperative Session Types Thu, 15 Sep 2022 07:13:24 +0000 https://doi.org/10.46298/lmcs-18(3:33)2022 https://doi.org/10.46298/lmcs-18(3:33)2022 Saffrich, Hannes Thiemann, Peter Saffrich, Hannes Thiemann, Peter 0 A Functional Abstraction of Typed Invocation Contexts Thu, 15 Sep 2022 07:10:38 +0000 https://doi.org/10.46298/lmcs-18(3:34)2022 https://doi.org/10.46298/lmcs-18(3:34)2022 Cong, Youyou Ishio, Chiaki Honda, Kaho Asai, Kenichi Cong, Youyou Ishio, Chiaki Honda, Kaho Asai, Kenichi 0 Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model Mon, 12 Sep 2022 07:02:22 +0000 https://doi.org/10.46298/lmcs-18(3:32)2022 https://doi.org/10.46298/lmcs-18(3:32)2022 Díaz-Caro, Alejandro Malherbe, Octavio Díaz-Caro, Alejandro Malherbe, Octavio 0 Distributed Asynchronous Games With Causal Memory are Undecidable Thu, 08 Sep 2022 07:20:29 +0000 https://doi.org/10.46298/lmcs-18(3:30)2022 https://doi.org/10.46298/lmcs-18(3:30)2022 Gimbert, Hugo Gimbert, Hugo 0 Minimality Notions via Factorization Systems and Examples Thu, 08 Sep 2022 06:20:32 +0000 https://doi.org/10.46298/lmcs-18(3:31)2022 https://doi.org/10.46298/lmcs-18(3:31)2022 Wißmann, Thorsten Wißmann, Thorsten 0 The Theory of Universal Graphs for Infinite Duration Games Wed, 07 Sep 2022 15:25:53 +0000 https://doi.org/10.46298/lmcs-18(3:29)2022 https://doi.org/10.46298/lmcs-18(3:29)2022 Colcombet, Thomas Fijalkow, Nathanaël Gawrychowski, Paweł Ohlmann, Pierre Colcombet, Thomas Fijalkow, Nathanaël Gawrychowski, Paweł Ohlmann, Pierre 0 Linear Dependent Type Theory for Quantum Programming Languages Wed, 07 Sep 2022 06:58:06 +0000 https://doi.org/10.46298/lmcs-18(3:28)2022 https://doi.org/10.46298/lmcs-18(3:28)2022 Fu, Peng Kishida, Kohei Selinger, Peter Fu, Peng Kishida, Kohei Selinger, Peter 0 Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types Wed, 31 Aug 2022 19:58:15 +0000 https://doi.org/10.46298/lmcs-18(3:27)2022 https://doi.org/10.46298/lmcs-18(3:27)2022 Ciccone, Luca Padovani, Luca Ciccone, Luca Padovani, Luca 0 Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays Wed, 31 Aug 2022 19:57:35 +0000 https://doi.org/10.46298/lmcs-18(3:26)2022 https://doi.org/10.46298/lmcs-18(3:26)2022 Mann, Makai Irfan, Ahmed Griggio, Alberto Padon, Oded Barrett, Clark Mann, Makai Irfan, Ahmed Griggio, Alberto Padon, Oded Barrett, Clark 0 Disjunctive bases: normal forms and model theory for modal logics Mon, 22 Aug 2022 22:00:00 +0000 https://doi.org/10.23638/LMCS-15(1:30)2019 https://doi.org/10.23638/LMCS-15(1:30)2019 Enqvist, Sebastian Venema, Yde Enqvist, Sebastian Venema, Yde 0 Small Promise CSPs that reduce to large CSPs 1$ and every prime p we give A, B of size n with a single relation of arity $n^p$ such that PCSP(A, B) reduces via a chain of homomorphisms $ A\to C\to B$ to a tractable CSP over some C of size p but not over any smaller structure. In a second family of examples, for every prime $p\geq 7$ we construct A, B of size $p-1$ with a single ternary relation such that PCSP(A, B) reduces via $A\to C\to B$ to a tractable CSP over some C of size p but not over any smaller structure. In contrast we show that if A, B are graphs and PCSP(A,B) reduces to tractable CSP(C) for some finite digraph C, then already A or B has a tractable CSP. This extends results and answers a question of Deng et al.]]> Mon, 22 Aug 2022 10:10:14 +0000 https://doi.org/10.46298/lmcs-18(3:25)2022 https://doi.org/10.46298/lmcs-18(3:25)2022 Kazda, Alexandr Mayr, Peter Zhuk, Dmitriy Kazda, Alexandr Mayr, Peter Zhuk, Dmitriy 1$ and every prime p we give A, B of size n with a single relation of arity $n^p$ such that PCSP(A, B) reduces via a chain of homomorphisms $ A\to C\to B$ to a tractable CSP over some C of size p but not over any smaller structure. In a second family of examples, for every prime $p\geq 7$ we construct A, B of size $p-1$ with a single ternary relation such that PCSP(A, B) reduces via $A\to C\to B$ to a tractable CSP over some C of size p but not over any smaller structure. In contrast we show that if A, B are graphs and PCSP(A,B) reduces to tractable CSP(C) for some finite digraph C, then already A or B has a tractable CSP. This extends results and answers a question of Deng et al.]]> 0 Limits of real numbers in the binary signed digit representation Fri, 19 Aug 2022 12:24:49 +0000 https://doi.org/10.46298/lmcs-18(3:24)2022 https://doi.org/10.46298/lmcs-18(3:24)2022 Wiesnet, Franziskus Köpp, Nils Wiesnet, Franziskus Köpp, Nils 0 Strongly-Normalizing Higher-Order Relational Queries Wed, 17 Aug 2022 13:35:47 +0000 https://doi.org/10.46298/lmcs-18(3:23)2022 https://doi.org/10.46298/lmcs-18(3:23)2022 Ricciotti, Wilmer Cheney, James Ricciotti, Wilmer Cheney, James 0 Typability and Type Inference in Atomic Polymorphism Fri, 12 Aug 2022 06:50:08 +0000 https://doi.org/10.46298/lmcs-18(3:22)2022 https://doi.org/10.46298/lmcs-18(3:22)2022 Protin, M. Clarence Ferreira, Gilda Protin, M. Clarence Ferreira, Gilda 0 The Third Trick Tue, 09 Aug 2022 17:08:17 +0000 https://doi.org/10.46298/lmcs-18(3:21)2022 https://doi.org/10.46298/lmcs-18(3:21)2022 Diener, Hannes Hendtlass, Matthew Diener, Hannes Hendtlass, Matthew 0 Instance reducibility and Weihrauch degrees Tue, 09 Aug 2022 12:14:30 +0000 https://doi.org/10.46298/lmcs-18(3:20)2022 https://doi.org/10.46298/lmcs-18(3:20)2022 Bauer, Andrej Bauer, Andrej 0 Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy Tue, 09 Aug 2022 12:13:29 +0000 https://doi.org/10.46298/lmcs-18(3:19)2022 https://doi.org/10.46298/lmcs-18(3:19)2022 Bisping, Benjamin Jansen, David N. Nestmann, Uwe Bisping, Benjamin Jansen, David N. Nestmann, Uwe 0 Moss' logic for ordered coalgebras Tue, 09 Aug 2022 05:54:14 +0000 https://doi.org/10.46298/lmcs-18(3:18)2022 https://doi.org/10.46298/lmcs-18(3:18)2022 Bílková, Marta Dostál, Matěj Bílková, Marta Dostál, Matěj 0 One-Clock Priced Timed Games with Negative Weights Tue, 09 Aug 2022 05:53:27 +0000 https://doi.org/10.46298/lmcs-18(3:17)2022 https://doi.org/10.46298/lmcs-18(3:17)2022 Brihaye, Thomas Geeraerts, Gilles Haddad, Axel Lefaucheux, Engel Monmege, Benjamin Brihaye, Thomas Geeraerts, Gilles Haddad, Axel Lefaucheux, Engel Monmege, Benjamin 0 Differentials and distances in probabilistic coherence spaces Mon, 08 Aug 2022 16:48:26 +0000 https://doi.org/10.46298/lmcs-18(3:2)2022 https://doi.org/10.46298/lmcs-18(3:2)2022 Ehrhard, Thomas Ehrhard, Thomas 0 Modules over monads and operational semantics (expanded version) Tue, 02 Aug 2022 12:26:18 +0000 https://doi.org/10.46298/lmcs-18(3:3)2022 https://doi.org/10.46298/lmcs-18(3:3)2022 Hirschowitz, André Hirschowitz, Tom Lafont, Ambroise Hirschowitz, André Hirschowitz, Tom Lafont, Ambroise 0 Tameness and the power of programs over monoids in DA Tue, 02 Aug 2022 12:26:14 +0000 https://doi.org/10.46298/lmcs-18(3:14)2022 https://doi.org/10.46298/lmcs-18(3:14)2022 Grosshans, Nathan Mckenzie, Pierre Segoufin, Luc Grosshans, Nathan Mckenzie, Pierre Segoufin, Luc 0 Minimization and Canonization of GFG Transition-Based Automata Tue, 02 Aug 2022 09:38:49 +0000 https://doi.org/10.46298/lmcs-18(3:16)2022 https://doi.org/10.46298/lmcs-18(3:16)2022 Radi, Bader Abu Kupferman, Orna Radi, Bader Abu Kupferman, Orna 0 Point-free Construction of Real Exponentiation Tue, 02 Aug 2022 09:37:42 +0000 https://doi.org/10.46298/lmcs-18(3:15)2022 https://doi.org/10.46298/lmcs-18(3:15)2022 Ng, Ming Vickers, Steven Ng, Ming Vickers, Steven 0 Comparator automata in quantitative verification Fri, 29 Jul 2022 09:14:31 +0000 https://doi.org/10.46298/lmcs-18(3:13)2022 https://doi.org/10.46298/lmcs-18(3:13)2022 Bansal, Suguman Chaudhuri, Swarat Vardi, Moshe Y. Bansal, Suguman Chaudhuri, Swarat Vardi, Moshe Y. 0 Timed Automata Robustness Analysis via Model Checking Fri, 29 Jul 2022 09:13:14 +0000 https://doi.org/10.46298/lmcs-18(3:12)2022 https://doi.org/10.46298/lmcs-18(3:12)2022 Bendík, Jaroslav Sencan, Ahmet Gol, Ebru Aydin Černá, Ivana Bendík, Jaroslav Sencan, Ahmet Gol, Ebru Aydin Černá, Ivana 0 A First-Order Complete Temporal Logic for Structured Context-Free Languages Fri, 29 Jul 2022 09:12:05 +0000 https://doi.org/10.46298/lmcs-18(3:11)2022 https://doi.org/10.46298/lmcs-18(3:11)2022 Chiari, Michele Mandrioli, Dino Pradella, Matteo Chiari, Michele Mandrioli, Dino Pradella, Matteo 0 Addressing Machines as models of lambda-calculus Fri, 29 Jul 2022 09:10:35 +0000 https://doi.org/10.46298/lmcs-18(3:10)2022 https://doi.org/10.46298/lmcs-18(3:10)2022 Della Penna, Giuseppe Intrigila, Benedetto Manzonetto, Giulio Della Penna, Giuseppe Intrigila, Benedetto Manzonetto, Giulio 0 Computability of Data-Word Transductions over Different Data Domains Fri, 29 Jul 2022 09:09:26 +0000 https://doi.org/10.46298/lmcs-18(3:9)2022 https://doi.org/10.46298/lmcs-18(3:9)2022 Exibard, Léo Filiot, Emmanuel Lhote, Nathan Reynier, Pierre-Alain Exibard, Léo Filiot, Emmanuel Lhote, Nathan Reynier, Pierre-Alain 0 Modularising Verification Of Durable Opacity Thu, 28 Jul 2022 09:08:05 +0000 https://doi.org/10.46298/lmcs-18(3:7)2022 https://doi.org/10.46298/lmcs-18(3:7)2022 Bila, Eleni Derrick, John Doherty, Simon Dongol, Brijesh Schellhorn, Gerhard Wehrheim, Heike Bila, Eleni Derrick, John Doherty, Simon Dongol, Brijesh Schellhorn, Gerhard Wehrheim, Heike 0 Fusible numbers and Peano Arithmetic Thu, 28 Jul 2022 09:06:43 +0000 https://doi.org/10.46298/lmcs-18(3:6)2022 https://doi.org/10.46298/lmcs-18(3:6)2022 Erickson, Jeff Nivasch, Gabriel Xu, Junyan Erickson, Jeff Nivasch, Gabriel Xu, Junyan 0 Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? = 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.]]> Thu, 28 Jul 2022 09:04:03 +0000 https://doi.org/10.46298/lmcs-18(3:5)2022 https://doi.org/10.46298/lmcs-18(3:5)2022 Bednarczyk, Bartosz Demri, Stéphane Bednarczyk, Bartosz Demri, Stéphane = 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.]]> 0 Uniform Envelopes Wed, 27 Jul 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(3:8)2022 https://doi.org/10.46298/lmcs-18(3:8)2022 Neumann, Eike Neumann, Eike 0 A Coalgebraic Approach to Dualities for Neighborhood Frames Wed, 27 Jul 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(3:4)2022 https://doi.org/10.46298/lmcs-18(3:4)2022 Bezhanishvili, Guram Bezhanishvili, Nick de Groot, Jim Bezhanishvili, Guram Bezhanishvili, Nick de Groot, Jim 0 Modal meet-implication logic Wed, 13 Jul 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(3:1)2022 https://doi.org/10.46298/lmcs-18(3:1)2022 de Groot, Jim Pattinson, Dirk de Groot, Jim Pattinson, Dirk 0 Synthesis of Computable Regular Functions of Infinite Words Wed, 29 Jun 2022 07:55:29 +0000 https://doi.org/10.46298/lmcs-18(2:23)2022 https://doi.org/10.46298/lmcs-18(2:23)2022 Dave, V. Filiot, E. Krishna, S. Lhote, N. Dave, V. Filiot, E. Krishna, S. Lhote, N. 0 Asynchronous wreath product and cascade decompositions for concurrent behaviours Tue, 28 Jun 2022 09:55:59 +0000 https://doi.org/10.46298/lmcs-18(2:22)2022 https://doi.org/10.46298/lmcs-18(2:22)2022 Adsul, Bharat Gastin, Paul Sarkar, Saptarshi Weil, Pascal Adsul, Bharat Gastin, Paul Sarkar, Saptarshi Weil, Pascal 0 The Theory of Traces for Systems with Nondeterminism, Probability, and Termination Fri, 17 Jun 2022 08:28:25 +0000 https://doi.org/10.46298/lmcs-18(2:21)2022 https://doi.org/10.46298/lmcs-18(2:21)2022 Bonchi, Filippo Sokolova, Ana Vignudelli, Valeria Bonchi, Filippo Sokolova, Ana Vignudelli, Valeria 0 The Shapley Value of Inconsistency Measures for Functional Dependencies Wed, 15 Jun 2022 08:05:31 +0000 https://doi.org/10.46298/lmcs-18(2:20)2022 https://doi.org/10.46298/lmcs-18(2:20)2022 Livshits, Ester Kimelfeld, Benny Livshits, Ester Kimelfeld, Benny 0 Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions Wed, 15 Jun 2022 08:02:05 +0000 https://doi.org/10.46298/lmcs-18(2:19)2022 https://doi.org/10.46298/lmcs-18(2:19)2022 Wild, Paul Schröder, Lutz Wild, Paul Schröder, Lutz 0 Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers Tue, 14 Jun 2022 16:38:18 +0000 https://doi.org/10.46298/lmcs-18(2:18)2022 https://doi.org/10.46298/lmcs-18(2:18)2022 Hamana, Makoto Hamana, Makoto 0 Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens Tue, 14 Jun 2022 06:42:19 +0000 https://doi.org/10.46298/lmcs-18(2:17)2022 https://doi.org/10.46298/lmcs-18(2:17)2022 Kirst, Dominik Larchey-Wendling, Dominique Kirst, Dominik Larchey-Wendling, Dominique 0 A Finite-Model-Theoretic View on Propositional Proof Complexity Mon, 13 Jun 2022 22:00:00 +0000 https://doi.org/10.23638/LMCS-15(1:4)2019 https://doi.org/10.23638/LMCS-15(1:4)2019 Grädel, Erich Grohe, Martin Pago, Benedikt Pakusa, Wied Grädel, Erich Grohe, Martin Pago, Benedikt Pakusa, Wied 0 Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic Fri, 10 Jun 2022 14:06:09 +0000 https://doi.org/10.46298/lmcs-18(2:16)2022 https://doi.org/10.46298/lmcs-18(2:16)2022 Hinrichsen, Jonas Kastberg Bengtson, Jesper Krebbers, Robbert Hinrichsen, Jonas Kastberg Bengtson, Jesper Krebbers, Robbert 0 Quotients, inductive types, and quotient inductive types Tue, 07 Jun 2022 09:44:07 +0000 https://doi.org/10.46298/lmcs-18(2:15)2022 https://doi.org/10.46298/lmcs-18(2:15)2022 Fiore, Marcelo P. Pitts, Andrew M. Steenkamp, S. C. Fiore, Marcelo P. Pitts, Andrew M. Steenkamp, S. C. 0 When Can We Answer Queries Using Result-Bounded Data Interfaces? Thu, 02 Jun 2022 07:48:25 +0000 https://doi.org/10.46298/lmcs-18(2:14)2022 https://doi.org/10.46298/lmcs-18(2:14)2022 Amarilli, Antoine Benedikt, Michael Amarilli, Antoine Benedikt, Michael 0 Specification and Verification of Timing Properties in Interoperable Medical Systems Wed, 01 Jun 2022 07:38:04 +0000 https://doi.org/10.46298/lmcs-18(2:13)2022 https://doi.org/10.46298/lmcs-18(2:13)2022 Zarneshan, Mahsa Ghassemi, Fatemeh Khamespanah, Ehsan Sirjani, Marjan Hatcliff, John Zarneshan, Mahsa Ghassemi, Fatemeh Khamespanah, Ehsan Sirjani, Marjan Hatcliff, John 0 CC-circuits and the expressive power of nilpotent algebras Wed, 25 May 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(2:12)2022 https://doi.org/10.46298/lmcs-18(2:12)2022 Kompatscher, Michael Kompatscher, Michael 0 Tractable Combinations of Temporal CSPs Wed, 25 May 2022 11:03:29 +0000 https://doi.org/10.46298/lmcs-18(2:11)2022 https://doi.org/10.46298/lmcs-18(2:11)2022 Bodirsky, Manuel Greiner, Johannes Rydval, Jakub Bodirsky, Manuel Greiner, Johannes Rydval, Jakub 0 Formalizing the Face Lattice of Polyhedra Wed, 18 May 2022 07:25:05 +0000 https://doi.org/10.46298/lmcs-18(2:10)2022 https://doi.org/10.46298/lmcs-18(2:10)2022 Allamigeon, Xavier Katz, Ricardo D. Strub, Pierre-Yves Allamigeon, Xavier Katz, Ricardo D. Strub, Pierre-Yves 0 Circular Proofs as Session-Typed Processes: A Local Validity Condition Tue, 10 May 2022 16:26:24 +0000 https://doi.org/10.46298/lmcs-18(2:8)2022 https://doi.org/10.46298/lmcs-18(2:8)2022 Derakhshan, Farzaneh Pfenning, Frank Derakhshan, Farzaneh Pfenning, Frank 0 Determinisability of register and timed automata Tue, 10 May 2022 07:36:52 +0000 https://doi.org/10.46298/lmcs-18(2:9)2022 https://doi.org/10.46298/lmcs-18(2:9)2022 Clemente, Lorenzo Lasota, Sławomir Piórkowski, Radosław Clemente, Lorenzo Lasota, Sławomir Piórkowski, Radosław 0 Enumerating Answers to First-Order Queries over Databases of Low Degree 0$, all but finitely many databases in the class have degree at most $n^{\delta}$, where $n$ is the size of the database. Typical examples are databases of bounded degree or of degree bounded by $\log n$. It is known that over a class of databases having low degree, first-order boolean queries can be checked in pseudo-linear time, i.e.\ for all $\epsilon>0$ in time bounded by $n^{1+\epsilon}$. We generalize this result by considering query evaluation. We show that counting the number of answers to a query can be done in pseudo-linear time and that after a pseudo-linear time preprocessing we can test in constant time whether a given tuple is a solution to a query or enumerate the answers to a query with constant delay.]]> Tue, 10 May 2022 07:35:46 +0000 https://doi.org/10.46298/lmcs-18(2:7)2022 https://doi.org/10.46298/lmcs-18(2:7)2022 Durand, Arnaud Schweikardt, Nicole Segoufin, Luc Durand, Arnaud Schweikardt, Nicole Segoufin, Luc 0$, all but finitely many databases in the class have degree at most $n^{\delta}$, where $n$ is the size of the database. Typical examples are databases of bounded degree or of degree bounded by $\log n$. It is known that over a class of databases having low degree, first-order boolean queries can be checked in pseudo-linear time, i.e.\ for all $\epsilon>0$ in time bounded by $n^{1+\epsilon}$. We generalize this result by considering query evaluation. We show that counting the number of answers to a query can be done in pseudo-linear time and that after a pseudo-linear time preprocessing we can test in constant time whether a given tuple is a solution to a query or enumerate the answers to a query with constant delay.]]> 0 A Near-Optimal Parallel Algorithm for Joining Binary Relations Wed, 04 May 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(2:6)2022 https://doi.org/10.46298/lmcs-18(2:6)2022 Ketsman, Bas Suciu, Dan Tao, Yufei Ketsman, Bas Suciu, Dan Tao, Yufei 0 Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms Tue, 26 Apr 2022 07:07:52 +0000 https://doi.org/10.46298/lmcs-18(2:5)2022 https://doi.org/10.46298/lmcs-18(2:5)2022 Faggian, Claudia Faggian, Claudia 0 Gluing resource proof-structures: inhabitation and inverting the Taylor expansion Fri, 22 Apr 2022 08:52:27 +0000 https://doi.org/10.46298/lmcs-18(2:4)2022 https://doi.org/10.46298/lmcs-18(2:4)2022 Guerrieri, Giulio Pellissier, Luc de Falco, Lorenzo Tortora Guerrieri, Giulio Pellissier, Luc de Falco, Lorenzo Tortora 0 A Flexible Proof Format for SAT Solver-Elaborator Communication 84% median reduction in elaboration time and >94% median decrease in peak memory usage.]]> Mon, 18 Apr 2022 10:47:09 +0000 https://doi.org/10.46298/lmcs-18(2:3)2022 https://doi.org/10.46298/lmcs-18(2:3)2022 Baek, Seulkee Carneiro, Mario Heule, Marijn J. H. Baek, Seulkee Carneiro, Mario Heule, Marijn J. H. 84% median reduction in elaboration time and >94% median decrease in peak memory usage.]]> 0 Uniform Interpolants in EUF: Algorithms using DAG-representations Wed, 13 Apr 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(2:2)2022 https://doi.org/10.46298/lmcs-18(2:2)2022 Ghilardi, Silvio Gianola, Alessandro Kapur, Deepak Ghilardi, Silvio Gianola, Alessandro Kapur, Deepak 0 Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages Tue, 12 Apr 2022 22:00:00 +0000 https://doi.org/10.46298/lmcs-18(2:1)2022 https://doi.org/10.46298/lmcs-18(2:1)2022 Ullrich, Sebastian de Moura, Leonardo Ullrich, Sebastian de Moura, Leonardo 0 A Cubical Language for Bishop Sets Tue, 29 Mar 2022 07:29:14 +0000 https://doi.org/10.46298/lmcs-18(1:43)2022 https://doi.org/10.46298/lmcs-18(1:43)2022 Sterling, Jonathan Angiuli, Carlo Gratzer, Daniel Sterling, Jonathan Angiuli, Carlo Gratzer, Daniel 0 Register Automata with Extrema Constraints, and an Application to Two-Variable Logic Wed, 23 Mar 2022 12:37:11 +0000 https://doi.org/10.46298/lmcs-18(1:42)2022 https://doi.org/10.46298/lmcs-18(1:42)2022 Toruńczyk, Szymon Zeume, Thomas Toruńczyk, Szymon Zeume, Thomas 0 Higher Order Automatic Differentiation of Higher Order Functions Tue, 22 Mar 2022 08:24:47 +0000 https://doi.org/10.46298/lmcs-18(1:41)2022 https://doi.org/10.46298/lmcs-18(1:41)2022 Huot, Mathieu Staton, Sam Vákár, Matthijs Huot, Mathieu Staton, Sam Vákár, Matthijs 0 The Big-O Problem Tue, 15 Mar 2022 15:54:03 +0000 https://doi.org/10.46298/lmcs-18(1:40)2022 https://doi.org/10.46298/lmcs-18(1:40)2022 Chistikov, Dmitry Kiefer, Stefan Murawski, Andrzej S. Purser, David Chistikov, Dmitry Kiefer, Stefan Murawski, Andrzej S. Purser, David 0 A Scalable Algorithm for Decentralized Actor Termination Detection Thu, 10 Mar 2022 23:00:00 +0000 https://doi.org/10.46298/lmcs-18(1:39)2022 https://doi.org/10.46298/lmcs-18(1:39)2022 Plyukhin, Dan Agha, Gul Plyukhin, Dan Agha, Gul 0 BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs Thu, 10 Mar 2022 17:35:31 +0000 https://doi.org/10.46298/lmcs-18(1:38)2022 https://doi.org/10.46298/lmcs-18(1:38)2022 Beneš, Nikola Brim, Luboš Pastva, Samuel Šafránek, David Beneš, Nikola Brim, Luboš Pastva, Samuel Šafránek, David 0 Sequential Relational Decomposition Thu, 03 Mar 2022 08:19:03 +0000 https://doi.org/10.46298/lmcs-18(1:37)2022 https://doi.org/10.46298/lmcs-18(1:37)2022 Fried, Dror Legay, Axel Ouaknine, Joël Vardi, Moshe Y. Fried, Dror Legay, Axel Ouaknine, Joël Vardi, Moshe Y. 0 Hilbert's Tenth Problem in Coq (Extended Version) Tue, 01 Mar 2022 10:42:30 +0000 https://doi.org/10.46298/lmcs-18(1:35)2022 https://doi.org/10.46298/lmcs-18(1:35)2022 Larchey-Wendling, Dominique Forster, Yannick Larchey-Wendling, Dominique Forster, Yannick 0 Verified Approximation Algorithms Tue, 01 Mar 2022 07:45:04 +0000 https://doi.org/10.46298/lmcs-18(1:36)2022 https://doi.org/10.46298/lmcs-18(1:36)2022 Eßmann, Robin Nipkow, Tobias Robillard, Simon Sulejmani, Ujkan Eßmann, Robin Nipkow, Tobias Robillard, Simon Sulejmani, Ujkan 0 Infinite Probabilistic Databases Fri, 25 Feb 2022 12:27:52 +0000 https://doi.org/10.46298/lmcs-18(1:34)2022 https://doi.org/10.46298/lmcs-18(1:34)2022 Grohe, Martin Lindner, Peter Grohe, Martin Lindner, Peter 0 A tier-based typed programming language characterizing Feasible Functionals Thu, 24 Feb 2022 08:38:31 +0000 https://doi.org/10.46298/lmcs-18(1:33)2022 https://doi.org/10.46298/lmcs-18(1:33)2022 Hainry, Emmanuel Kapron, Bruce M. Marion, Jean-Yves Péchoux, Romain Hainry, Emmanuel Kapron, Bruce M. Marion, Jean-Yves Péchoux, Romain 0 Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) Mon, 21 Feb 2022 23:00:00 +0000 https://doi.org/10.23638/LMCS-16(1:15)2020 https://doi.org/10.23638/LMCS-16(1:15)2020 Castagna, Giuseppe Castagna, Giuseppe 0 Proof Theory of Riesz Spaces and Modal Riesz Spaces Wed, 16 Feb 2022 23:00:00 +0000 https://doi.org/10.46298/lmcs-18(1:32)2022 https://doi.org/10.46298/lmcs-18(1:32)2022 Lucas, Christophe Mio, Matteo Lucas, Christophe Mio, Matteo 0 Reachability and liveness in parametric timed automata Wed, 09 Feb 2022 12:00:42 +0000 https://doi.org/10.46298/lmcs-18(1:31)2022 https://doi.org/10.46298/lmcs-18(1:31)2022 André, Étienne Lime, Didier Roux, Olivier H. André, Étienne Lime, Didier Roux, Olivier H. 0 Fixed Points Theorems for Non-Transitive Relations Thu, 03 Feb 2022 23:00:00 +0000 https://doi.org/10.46298/lmcs-18(1:30)2022 https://doi.org/10.46298/lmcs-18(1:30)2022 Dubut, Jérémy Yamada, Akihisa Dubut, Jérémy Yamada, Akihisa 0 Duality for powerset coalgebras Thu, 03 Feb 2022 13:48:06 +0000 https://doi.org/10.46298/lmcs-18(1:27)2022 https://doi.org/10.46298/lmcs-18(1:27)2022 Bezhanishvili, Guram Carai, Luca Morandi, Patrick Bezhanishvili, Guram Carai, Luca Morandi, Patrick 0 Canonicity and homotopy canonicity for cubical type theory Thu, 03 Feb 2022 13:46:29 +0000 https://doi.org/10.46298/lmcs-18(1:28)2022 https://doi.org/10.46298/lmcs-18(1:28)2022 Coquand, Thierry Huber, Simon Sattler, Christian Coquand, Thierry Huber, Simon Sattler, Christian 0 Residuality and Learning for Nondeterministic Nominal Automata Thu, 03 Feb 2022 10:51:59 +0000 https://doi.org/10.46298/lmcs-18(1:29)2022 https://doi.org/10.46298/lmcs-18(1:29)2022 Moerman, Joshua Sammartino, Matteo Moerman, Joshua Sammartino, Matteo 0 Optimizing tree decompositions in MSO Wed, 02 Feb 2022 23:00:00 +0000 https://doi.org/10.46298/lmcs-18(1:26)2022 https://doi.org/10.46298/lmcs-18(1:26)2022 Bojańczyk, Mikołaj Pilipczuk, Michał Bojańczyk, Mikołaj Pilipczuk, Michał 0 Verifying liquidity of recursive Bitcoin contracts Tue, 01 Feb 2022 15:49:52 +0000 https://doi.org/10.46298/lmcs-18(1:22)2022 https://doi.org/10.46298/lmcs-18(1:22)2022 Bartoletti, Massimo Lande, Stefano Murgia, Maurizio Zunino, Roberto Bartoletti, Massimo Lande, Stefano Murgia, Maurizio Zunino, Roberto 0 Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption Tue, 01 Feb 2022 14:15:37 +0000 https://doi.org/10.46298/lmcs-18(1:24)2022 https://doi.org/10.46298/lmcs-18(1:24)2022 Bozzelli, Laura Molinari, Alberto Montanari, Angelo Peron, Adriano Sala, Pietro Bozzelli, Laura Molinari, Alberto Montanari, Angelo Peron, Adriano Sala, Pietro 0 Regular matching problems for infinite trees Tue, 01 Feb 2022 08:24:11 +0000 https://doi.org/10.46298/lmcs-18(1:25)2022 https://doi.org/10.46298/lmcs-18(1:25)2022 Camino, Carlos Diekert, Volker Dundua, Besik Marin, Mircea Sénizergues, Géraud Camino, Carlos Diekert, Volker Dundua, Besik Marin, Mircea Sénizergues, Géraud 0 Quotients of Bounded Natural Functors Tue, 01 Feb 2022 08:22:28 +0000 https://doi.org/10.46298/lmcs-18(1:23)2022 https://doi.org/10.46298/lmcs-18(1:23)2022 Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy Fürer, Basil Lochbihler, Andreas Schneider, Joshua Traytel, Dmitriy 0 Weight Annotation in Information Extraction Mon, 31 Jan 2022 09:21:27 +0000 https://doi.org/10.46298/lmcs-18(1:21)2022 https://doi.org/10.46298/lmcs-18(1:21)2022 Doleschal, Johannes Kimelfeld, Benny Martens, Wim Peterfreund, Liat Doleschal, Johannes Kimelfeld, Benny Martens, Wim Peterfreund, Liat 0 Quantifying over Boolean announcements Fri, 21 Jan 2022 12:23:37 +0000 https://doi.org/10.46298/lmcs-18(1:20)2022 https://doi.org/10.46298/lmcs-18(1:20)2022 van Ditmarsch, Hans French, Tim van Ditmarsch, Hans French, Tim 0 On the Nielsen-Schreier Theorem in Homotopy Type Theory Thu, 20 Jan 2022 14:26:48 +0000 https://doi.org/10.46298/lmcs-18(1:18)2022 https://doi.org/10.46298/lmcs-18(1:18)2022 Swan, Andrew W Swan, Andrew W 0 Bounded Reachability Problems are Decidable in FIFO Machines Wed, 19 Jan 2022 23:00:00 +0000 https://doi.org/10.46298/lmcs-18(1:19)2022 https://doi.org/10.46298/lmcs-18(1:19)2022 Bollig, Benedikt Finkel, Alain Suresh, Amrita Bollig, Benedikt Finkel, Alain Suresh, Amrita 0 An extensible equality checking algorithm for dependent type theories Wed, 19 Jan 2022 12:16:59 +0000 https://doi.org/10.46298/lmcs-18(1:17)2022 https://doi.org/10.46298/lmcs-18(1:17)2022 Bauer, Andrej Komel, Anja Petković Bauer, Andrej Komel, Anja Petković 0 On the Axiomatisability of Parallel Composition Wed, 19 Jan 2022 12:14:36 +0000 https://doi.org/10.46298/lmcs-18(1:15)2022 https://doi.org/10.46298/lmcs-18(1:15)2022 Aceto, Luca Castiglioni, Valentina Ingolfsdottir, Anna Luttik, Bas Pedersen, Mathias R. Aceto, Luca Castiglioni, Valentina Ingolfsdottir, Anna Luttik, Bas Pedersen, Mathias R. 0 A duality theoretic view on limits of finite structures: Extended version Wed, 19 Jan 2022 12:11:21 +0000 https://doi.org/10.46298/lmcs-18(1:16)2022 https://doi.org/10.46298/lmcs-18(1:16)2022 Gehrke, Mai Jakl, Tomáš Reggio, Luca Gehrke, Mai Jakl, Tomáš Reggio, Luca 0 Universal Algebraic Methods for Constraint Satisfaction Problems Wed, 19 Jan 2022 09:44:46 +0000 https://doi.org/10.46298/lmcs-18(1:12)2022 https://doi.org/10.46298/lmcs-18(1:12)2022 Bergman, Clifford DeMeo, William Bergman, Clifford DeMeo, William 0 Conformance Relations and Hyperproperties for Doping Detection in Time and Space Wed, 19 Jan 2022 09:42:18 +0000 https://doi.org/10.46298/lmcs-18(1:14)2022 https://doi.org/10.46298/lmcs-18(1:14)2022 Biewer, Sebastian Dimitrova, Rayna Fries, Michael Gazda, Maciej Heinze, Thomas Hermanns, Holger Mousavi, Mohammad Reza Biewer, Sebastian Dimitrova, Rayna Fries, Michael Gazda, Maciej Heinze, Thomas Hermanns, Holger Mousavi, Mohammad Reza 0 No-Go Theorems for Distributive Laws Wed, 19 Jan 2022 09:38:58 +0000 https://doi.org/10.46298/lmcs-18(1:13)2022 https://doi.org/10.46298/lmcs-18(1:13)2022 Zwart, Maaike Marsden, Dan Zwart, Maaike Marsden, Dan 0 Games Where You Can Play Optimally with Arena-Independent Finite Memory Mon, 17 Jan 2022 11:22:32 +0000 https://doi.org/10.46298/lmcs-18(1:11)2022 https://doi.org/10.46298/lmcs-18(1:11)2022 Bouyer, Patricia Roux, Stéphane Le Oualhadj, Youssouf Randour, Mickael Vandenhove, Pierre Bouyer, Patricia Roux, Stéphane Le Oualhadj, Youssouf Randour, Mickael Vandenhove, Pierre 0 Normalization for planar string diagrams and a quadratic equivalence algorithm Fri, 14 Jan 2022 12:04:35 +0000 https://doi.org/10.46298/lmcs-18(1:10)2022 https://doi.org/10.46298/lmcs-18(1:10)2022 Delpeuch, Antonin Vicary, Jamie Delpeuch, Antonin Vicary, Jamie 0 Rast: A Language for Resource-Aware Session Types Wed, 12 Jan 2022 07:21:18 +0000 https://doi.org/10.46298/lmcs-18(1:9)2022 https://doi.org/10.46298/lmcs-18(1:9)2022 Das, Ankush Pfenning, Frank Das, Ankush Pfenning, Frank 0 A Recursive Approach to Solving Parity Games in Quasipolynomial Time Wed, 12 Jan 2022 07:19:45 +0000 https://doi.org/10.46298/lmcs-18(1:8)2022 https://doi.org/10.46298/lmcs-18(1:8)2022 Lehtinen, Karoliina Parys, Paweł Schewe, Sven Wojtczak, Dominik Lehtinen, Karoliina Parys, Paweł Schewe, Sven Wojtczak, Dominik 0 $\sigma$-locales in Formal Topology Wed, 12 Jan 2022 07:16:47 +0000 https://doi.org/10.46298/lmcs-18(1:7)2022 https://doi.org/10.46298/lmcs-18(1:7)2022 Ciraulo, Francesco Ciraulo, Francesco 0 Conditional Bisimilarity for Reactive Systems Wed, 12 Jan 2022 07:14:15 +0000 https://doi.org/10.46298/lmcs-18(1:6)2022 https://doi.org/10.46298/lmcs-18(1:6)2022 Hülsbusch, Mathias König, Barbara Küpper, Sebastian Stoltenow, Lars Hülsbusch, Mathias König, Barbara Küpper, Sebastian Stoltenow, Lars 0 Integrity Constraints Revisited: From Exact to Approximate Implication Tue, 11 Jan 2022 08:46:58 +0000 https://doi.org/10.46298/lmcs-18(1:5)2022 https://doi.org/10.46298/lmcs-18(1:5)2022 Kenig, Batya Suciu, Dan Kenig, Batya Suciu, Dan 0 The Dichotomy of Evaluating Homomorphism-Closed Queries on Probabilistic Graphs Fri, 07 Jan 2022 10:04:27 +0000 https://doi.org/10.46298/lmcs-18(1:2)2022 https://doi.org/10.46298/lmcs-18(1:2)2022 Amarilli, Antoine Ceylan, İsmail İlkan Amarilli, Antoine Ceylan, İsmail İlkan 0 A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems Fri, 07 Jan 2022 07:48:52 +0000 https://doi.org/10.46298/lmcs-18(1:4)2022 https://doi.org/10.46298/lmcs-18(1:4)2022 Nenzi, L. Bartocci, E. Bortolussi, L. Loreti, M. Nenzi, L. Bartocci, E. Bortolussi, L. Loreti, M. 0 Good-for-games $\omega$-Pushdown Automata Fri, 07 Jan 2022 07:46:44 +0000 https://doi.org/10.46298/lmcs-18(1:3)2022 https://doi.org/10.46298/lmcs-18(1:3)2022 Lehtinen, Karoliina Zimmermann, Martin Lehtinen, Karoliina Zimmermann, Martin 0 On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants Thu, 06 Jan 2022 07:47:46 +0000 https://doi.org/10.46298/lmcs-18(1:1)2022 https://doi.org/10.46298/lmcs-18(1:1)2022 Olimpieri, Federico Auclair, Lionel Vaux Olimpieri, Federico Auclair, Lionel Vaux 0 Architectures in parametric component-based systems: Qualitative and quantitative modelling Thu, 30 Dec 2021 14:19:44 +0000 https://doi.org/10.46298/lmcs-17(4:26)2021 https://doi.org/10.46298/lmcs-17(4:26)2021 Pittou, Maria Rahonis, George Pittou, Maria Rahonis, George 0 On Higher-Order Probabilistic Subrecursion Thu, 23 Dec 2021 16:26:36 +0000 https://doi.org/10.46298/lmcs-17(4:25)2021 https://doi.org/10.46298/lmcs-17(4:25)2021 Breuvart, Flavien Lago, Ugo Dal Herrou, Agathe Breuvart, Flavien Lago, Ugo Dal Herrou, Agathe 0 A coalgebraic take on regular and $\omega$-regular behaviours Thu, 23 Dec 2021 09:18:01 +0000 https://doi.org/10.46298/lmcs-17(4:24)2021 https://doi.org/10.46298/lmcs-17(4:24)2021 Brengos, Tomasz Brengos, Tomasz 0 Parametricity for Nested Types and GADTs Thu, 23 Dec 2021 09:14:58 +0000 https://doi.org/10.46298/lmcs-17(4:23)2021 https://doi.org/10.46298/lmcs-17(4:23)2021 Johann, Patricia Ghiorzi, Enrico Johann, Patricia Ghiorzi, Enrico 0 Stashing And Parallelization Pentagons Mon, 20 Dec 2021 16:56:19 +0000 https://doi.org/10.46298/lmcs-17(4:20)2021 https://doi.org/10.46298/lmcs-17(4:20)2021 Brattka, Vasco Brattka, Vasco 0 An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets Mon, 20 Dec 2021 16:40:43 +0000 https://doi.org/10.46298/lmcs-17(4:22)2021 https://doi.org/10.46298/lmcs-17(4:22)2021 Chouquet, Jules Auclair, Lionel Vaux Chouquet, Jules Auclair, Lionel Vaux 0 Adaptive Non-linear Pattern Matching Automata Fri, 17 Dec 2021 09:16:29 +0000 https://doi.org/10.46298/lmcs-17(4:21)2021 https://doi.org/10.46298/lmcs-17(4:21)2021 Erkens, Rick Laveaux, Maurice Erkens, Rick Laveaux, Maurice 0 Expressive Logics for Coinductive Predicates Wed, 15 Dec 2021 20:02:34 +0000 https://doi.org/10.46298/lmcs-17(4:19)2021 https://doi.org/10.46298/lmcs-17(4:19)2021 Kupke, Clemens Rot, Jurriaan Kupke, Clemens Rot, Jurriaan 0 Efficient Full Higher-Order Unification Tue, 14 Dec 2021 07:54:26 +0000 https://doi.org/10.46298/lmcs-17(4:18)2021 https://doi.org/10.46298/lmcs-17(4:18)2021 Vukmirović, Petar Bentkamp, Alexander Nummelin, Visa Vukmirović, Petar Bentkamp, Alexander Nummelin, Visa 0 A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm 0$ such that any $r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$ contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of which breaks the hypergraph into connected components with at most $m/2$ edges. We use this to give an algorithm running in time $d^{(1 - \epsilon_r)m}$ that decides satisfiability of $m$-variable $(d, k)$-CSPs in which every variable appears in at most $r$ constraints, where $\epsilon_r$ depends only on $r$ and $k\in o(\sqrt{m})$. Furthermore our algorithm solves the corresponding #CSP-SAT and Max-CSP-SAT of these CSPs. We also show that CNF representations of unsatisfiable $(2, k)$-CSPs with variable frequency $r$ can be refuted in tree-like resolution in size $2^{(1 - \epsilon_r)m}$. Furthermore for Tseitin formulas on graphs with degree at most $k$ (which are $(2, k)$-CSPs) we give a deterministic algorithm finding such a refutation.]]> Mon, 13 Dec 2021 13:56:52 +0000 https://doi.org/10.46298/lmcs-17(4:17)2021 https://doi.org/10.46298/lmcs-17(4:17)2021 Koucký, Michal Rödl, Vojtěch Talebanfard, Navid Koucký, Michal Rödl, Vojtěch Talebanfard, Navid 0$ such that any $r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$ contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of which breaks the hypergraph into connected components with at most $m/2$ edges. We use this to give an algorithm running in time $d^{(1 - \epsilon_r)m}$ that decides satisfiability of $m$-variable $(d, k)$-CSPs in which every variable appears in at most $r$ constraints, where $\epsilon_r$ depends only on $r$ and $k\in o(\sqrt{m})$. Furthermore our algorithm solves the corresponding #CSP-SAT and Max-CSP-SAT of these CSPs. We also show that CNF representations of unsatisfiable $(2, k)$-CSPs with variable frequency $r$ can be refuted in tree-like resolution in size $2^{(1 - \epsilon_r)m}$. Furthermore for Tseitin formulas on graphs with degree at most $k$ (which are $(2, k)$-CSPs) we give a deterministic algorithm finding such a refutation.]]> 0 A new operational representation of dependencies in Event Structures Thu, 02 Dec 2021 11:28:07 +0000 https://doi.org/10.46298/lmcs-17(4:16)2021 https://doi.org/10.46298/lmcs-17(4:16)2021 Pinna, G. Michele Pinna, G. Michele 0 A Probabilistic Higher-order Fixpoint Logic Thu, 02 Dec 2021 11:26:43 +0000 https://doi.org/10.46298/lmcs-17(4:15)2021 https://doi.org/10.46298/lmcs-17(4:15)2021 Mitani, Yo Kobayashi, Naoki Tsukada, Takeshi Mitani, Yo Kobayashi, Naoki Tsukada, Takeshi 0 On Supergraphs Satisfying CMSO Properties Mon, 29 Nov 2021 10:11:16 +0000 https://doi.org/10.46298/lmcs-17(4:14)2021 https://doi.org/10.46298/lmcs-17(4:14)2021 Oliveira, Mateus de Oliveira Oliveira, Mateus de Oliveira 0 Time-Fluid Field-Based Coordination through Programmable Distributed Schedulers Thu, 25 Nov 2021 07:35:50 +0000 https://doi.org/10.46298/lmcs-17(4:13)2021 https://doi.org/10.46298/lmcs-17(4:13)2021 Pianini, Danilo Casadei, Roberto Viroli, Mirko Mariani, Stefano Zambonelli, Franco Pianini, Danilo Casadei, Roberto Viroli, Mirko Mariani, Stefano Zambonelli, Franco 0 Controlling a random population Wed, 24 Nov 2021 08:35:03 +0000 https://doi.org/10.46298/lmcs-17(4:12)2021 https://doi.org/10.46298/lmcs-17(4:12)2021 Colcombet, Thomas Fijalkow, Nathanaël Ohlmann, Pierre Colcombet, Thomas Fijalkow, Nathanaël Ohlmann, Pierre 0 Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism Wed, 24 Nov 2021 08:34:51 +0000 https://doi.org/10.46298/lmcs-17(4:11)2021 https://doi.org/10.46298/lmcs-17(4:11)2021 Laird, James Laird, James 0 A theory of transaction parallelism in blockchains Thu, 18 Nov 2021 13:23:09 +0000 https://doi.org/10.46298/lmcs-17(4:10)2021 https://doi.org/10.46298/lmcs-17(4:10)2021 Bartoletti, Massimo Galletta, Letterio Murgia, Maurizio Bartoletti, Massimo Galletta, Letterio Murgia, Maurizio 0 Dagger linear logic for categorical quantum mechanics Mon, 15 Nov 2021 23:00:00 +0000 https://doi.org/10.46298/lmcs-17(4:8)2021 https://doi.org/10.46298/lmcs-17(4:8)2021 Cockett, Robin Comfort, Cole Srinivasan, Priyaa Cockett, Robin Comfort, Cole Srinivasan, Priyaa 0 Dynamic Complexity of Parity Exists Queries Mon, 15 Nov 2021 23:00:00 +0000 https://doi.org/10.46298/lmcs-17(4:9)2021 https://doi.org/10.46298/lmcs-17(4:9)2021 Vortmeier, Nils Zeume, Thomas Vortmeier, Nils Zeume, Thomas 0 Tight Polynomial Bounds for Loop Programs in Polynomial Space Thu, 11 Nov 2021 08:30:00 +0000 https://doi.org/10.46298/lmcs-17(4:7)2021 https://doi.org/10.46298/lmcs-17(4:7)2021 Ben-Amram, A. M. Hamilton, G. W. Ben-Amram, A. M. Hamilton, G. W. 0 Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities Wed, 03 Nov 2021 08:33:20 +0000 https://doi.org/10.46298/lmcs-17(4:6)2021 https://doi.org/10.46298/lmcs-17(4:6)2021 Sproston, Jeremy Sproston, Jeremy 0 Internal Parametricity for Cubical Type Theory Wed, 03 Nov 2021 08:31:47 +0000 https://doi.org/10.46298/lmcs-17(4:5)2021 https://doi.org/10.46298/lmcs-17(4:5)2021 Cavallo, Evan Harper, Robert Cavallo, Evan Harper, Robert 0 Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility Thu, 28 Oct 2021 22:00:00 +0000 https://doi.org/10.46298/lmcs-17(4:4)2021 https://doi.org/10.46298/lmcs-17(4:4)2021 Lin, Anthony W. Majumdar, Rupak Lin, Anthony W. Majumdar, Rupak 0 Modal Functional (Dialectica) Interpretation Mon, 25 Oct 2021 15:32:37 +0000 https://doi.org/10.46298/lmcs-17(4:3)2021 https://doi.org/10.46298/lmcs-17(4:3)2021 Hernest, Dan Trifonov, Trifon Hernest, Dan Trifonov, Trifon 0 Causal Consistency for Reversible Multiparty Protocols Fri, 01 Oct 2021 07:11:49 +0000 https://doi.org/10.46298/lmcs-17(4:1)2021 https://doi.org/10.46298/lmcs-17(4:1)2021 Mezzina, Claudio Antares Pérez, Jorge A. Mezzina, Claudio Antares Pérez, Jorge A. 0 Foundations of regular coinduction Fri, 01 Oct 2021 07:09:33 +0000 https://doi.org/10.46298/lmcs-17(4:2)2021 https://doi.org/10.46298/lmcs-17(4:2)2021 Dagnino, Francesco Dagnino, Francesco 0 W-types in setoids Fri, 24 Sep 2021 14:08:03 +0000 https://doi.org/10.46298/lmcs-17(3:28)2021 https://doi.org/10.46298/lmcs-17(3:28)2021 Emmenegger, Jacopo Emmenegger, Jacopo 0 Modular Path Queries with Arithmetic Mon, 20 Sep 2021 08:36:59 +0000 https://doi.org/10.46298/lmcs-17(3:27)2021 https://doi.org/10.46298/lmcs-17(3:27)2021 Michaliszyn, Jakub Otop, Jan Wieczorek, Piotr Michaliszyn, Jakub Otop, Jan Wieczorek, Piotr 0 Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models Fri, 17 Sep 2021 11:43:13 +0000 https://doi.org/10.46298/lmcs-17(3:26)2021 https://doi.org/10.46298/lmcs-17(3:26)2021 Shimi, Adam Hurault, Aurélie Queinnec, Philippe Shimi, Adam Hurault, Aurélie Queinnec, Philippe 0 Modular coinduction up-to for higher-order languages via first-order transition systems Fri, 17 Sep 2021 07:46:50 +0000 https://doi.org/10.46298/lmcs-17(3:25)2021 https://doi.org/10.46298/lmcs-17(3:25)2021 Madiot, Jean-Marie Pous, Damien Sangiorgi, Davide Madiot, Jean-Marie Pous, Damien Sangiorgi, Davide 0 Separation for dot-depth two Fri, 17 Sep 2021 07:39:25 +0000 https://doi.org/10.46298/lmcs-17(3:24)2021 https://doi.org/10.46298/lmcs-17(3:24)2021 Place, Thomas Zeitoun, Marc Place, Thomas Zeitoun, Marc 0 Cartesian Difference Categories Tue, 07 Sep 2021 07:17:09 +0000 https://doi.org/10.46298/lmcs-17(3:23)2021 https://doi.org/10.46298/lmcs-17(3:23)2021 Alvarez-Picallo, Mario Lemay, Jean-Simon Pacaud Alvarez-Picallo, Mario Lemay, Jean-Simon Pacaud 0 The Shapley Value of Tuples in Query Answering Thu, 02 Sep 2021 06:15:54 +0000 https://doi.org/10.46298/lmcs-17(3:22)2021 https://doi.org/10.46298/lmcs-17(3:22)2021 Livshits, Ester Bertossi, Leopoldo Kimelfeld, Benny Sebag, Moshe Livshits, Ester Bertossi, Leopoldo Kimelfeld, Benny Sebag, Moshe 0 A program for the full axiom of choice Wed, 01 Sep 2021 14:21:30 +0000 https://doi.org/10.46298/lmcs-17(3:21)2021 https://doi.org/10.46298/lmcs-17(3:21)2021 Krivine, Jean-Louis Krivine, Jean-Louis 0 Equivalence checking for weak bi-Kleene algebra Fri, 13 Aug 2021 14:45:40 +0000 https://doi.org/10.46298/lmcs-17(3:19)2021 https://doi.org/10.46298/lmcs-17(3:19)2021 Kappé, Tobias Brunet, Paul Luttik, Bas Silva, Alexandra Zanasi, Fabio Kappé, Tobias Brunet, Paul Luttik, Bas Silva, Alexandra Zanasi, Fabio 0 Successor-Invariant First-Order Logic on Classes of Bounded Degree Fri, 13 Aug 2021 14:45:33 +0000 https://doi.org/10.46298/lmcs-17(3:20)2021 https://doi.org/10.46298/lmcs-17(3:20)2021 Grange, Julien Grange, Julien 0 Ambiguity Hierarchy of Regular Infinite Tree Languages 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over $\omega$-words every regular language is accepted by an unambiguous B\"uchi automaton and by a deterministic parity automaton. Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1 ambiguous; and there are finitely (respectively countably, uncountably) ambiguous languages that are not boundedly (respectively finitely, countably) ambiguous.]]> Fri, 13 Aug 2021 14:45:25 +0000 https://doi.org/10.46298/lmcs-17(3:18)2021 https://doi.org/10.46298/lmcs-17(3:18)2021 Rabinovich, Alexander Tiferet, Doron Rabinovich, Alexander Tiferet, Doron 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over $\omega$-words every regular language is accepted by an unambiguous B\"uchi automaton and by a deterministic parity automaton. Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1 ambiguous; and there are finitely (respectively countably, uncountably) ambiguous languages that are not boundedly (respectively finitely, countably) ambiguous.]]> 0 A Complete Axiomatisation for Quantifier-Free Separation Logic Tue, 10 Aug 2021 06:26:22 +0000 https://doi.org/10.46298/lmcs-17(3:17)2021 https://doi.org/10.46298/lmcs-17(3:17)2021 Demri, Stéphane Lozes, Étienne Mansutti, Alessio Demri, Stéphane Lozes, Étienne Mansutti, Alessio 0 Decision problems for linear recurrences involving arbitrary real numbers Tue, 10 Aug 2021 06:17:04 +0000 https://doi.org/10.46298/lmcs-17(3:16)2021 https://doi.org/10.46298/lmcs-17(3:16)2021 Neumann, Eike Neumann, Eike 0 A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic Tue, 10 Aug 2021 04:26:20 +0000 https://doi.org/10.46298/lmcs-17(3:2)2021 https://doi.org/10.46298/lmcs-17(3:2)2021 Ahn, Ki Yung Horne, Ross Tiu, Alwen Ahn, Ki Yung Horne, Ross Tiu, Alwen 0 On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics Fri, 30 Jul 2021 17:30:52 +0000 https://doi.org/10.46298/lmcs-17(3:14)2021 https://doi.org/10.46298/lmcs-17(3:14)2021 Hoelzel, Matthias Wilke, Richard Hoelzel, Matthias Wilke, Richard 0 Relating Apartness and Bisimulation Fri, 30 Jul 2021 06:50:54 +0000 https://doi.org/10.46298/lmcs-17(3:15)2021 https://doi.org/10.46298/lmcs-17(3:15)2021 Geuvers, Herman Jacobs, Bart Geuvers, Herman Jacobs, Bart 0 Representing Continuous Functions between Greatest Fixed Points of Indexed Containers Wed, 28 Jul 2021 08:28:02 +0000 https://doi.org/10.46298/lmcs-17(3:13)2021 https://doi.org/10.46298/lmcs-17(3:13)2021 Hyvernat, Pierre Hyvernat, Pierre 0 Multimodal Dependent Type Theory Wed, 28 Jul 2021 08:27:54 +0000 https://doi.org/10.46298/lmcs-17(3:11)2021 https://doi.org/10.46298/lmcs-17(3:11)2021 Gratzer, Daniel Kavvos, G. A. Nuyts, Andreas Birkedal, Lars Gratzer, Daniel Kavvos, G. A. Nuyts, Andreas Birkedal, Lars 0 On p/q-recognisable sets Wed, 28 Jul 2021 08:27:22 +0000 https://doi.org/10.46298/lmcs-17(3:12)2021 https://doi.org/10.46298/lmcs-17(3:12)2021 Marsault, Victor Marsault, Victor 0 Distribution Bisimilarity via the Power of Convex Algebras Fri, 23 Jul 2021 13:49:17 +0000 https://doi.org/10.46298/lmcs-17(3:10)2021 https://doi.org/10.46298/lmcs-17(3:10)2021 Bonchi, Filippo Silva, Alexandra Sokolova, Ana Bonchi, Filippo Silva, Alexandra Sokolova, Ana 0 Foundations of Online Structure Theory II: The Operator Approach Wed, 21 Jul 2021 17:27:13 +0000 https://doi.org/10.46298/lmcs-17(3:6)2021 https://doi.org/10.46298/lmcs-17(3:6)2021 Downey, Rod Melnikov, Alexander Ng, Keng Meng Downey, Rod Melnikov, Alexander Ng, Keng Meng 0 ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity Wed, 21 Jul 2021 12:11:56 +0000 https://doi.org/10.46298/lmcs-17(3:9)2021 https://doi.org/10.46298/lmcs-17(3:9)2021 Frumin, Dan Krebbers, Robbert Birkedal, Lars Frumin, Dan Krebbers, Robbert Birkedal, Lars 0 A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Wed, 21 Jul 2021 12:11:40 +0000 https://doi.org/10.46298/lmcs-17(3:8)2021 https://doi.org/10.46298/lmcs-17(3:8)2021 Neele, Thomas Valmari, Antti Willemse, Tim A. C. Neele, Thomas Valmari, Antti Willemse, Tim A. C. 0 Pumping lemmas for weighted automata Wed, 21 Jul 2021 06:01:45 +0000 https://doi.org/10.46298/lmcs-17(3:7)2021 https://doi.org/10.46298/lmcs-17(3:7)2021 Chattopadhyay, Agnishom Mazowiecki, Filip Muscholl, Anca Riveros, Cristian Chattopadhyay, Agnishom Mazowiecki, Filip Muscholl, Anca Riveros, Cristian 0 Axiomatizing Hybrid XPath with Data Tue, 20 Jul 2021 06:34:08 +0000 https://doi.org/10.46298/lmcs-17(3:5)2021 https://doi.org/10.46298/lmcs-17(3:5)2021 Areces, Carlos Fervari, Raul Areces, Carlos Fervari, Raul 0 Presburger Arithmetic with algebraic scalar multiplications 0$ only depend on $\alpha$, and $\ell(S)$ is the length of the given $\alpha$-PA sentence $S$. Furthermore deciding $\exists^{6}\forall^{4}\exists^{11}$ $\alpha$-PA sentences with at most $k$ inequalities is PSPACE-hard, where $k$ is another constant depending only on~$\alpha$. When $\alpha$ is non-quadratic, already four alternating quantifier blocks suffice for undecidability of $\alpha$-PA sentences.]]> Tue, 20 Jul 2021 06:32:31 +0000 https://doi.org/10.46298/lmcs-17(3:4)2021 https://doi.org/10.46298/lmcs-17(3:4)2021 Hieronymi, Philipp Nguyen, Danny Pak, Igor Hieronymi, Philipp Nguyen, Danny Pak, Igor 0$ only depend on $\alpha$, and $\ell(S)$ is the length of the given $\alpha$-PA sentence $S$. Furthermore deciding $\exists^{6}\forall^{4}\exists^{11}$ $\alpha$-PA sentences with at most $k$ inequalities is PSPACE-hard, where $k$ is another constant depending only on~$\alpha$. When $\alpha$ is non-quadratic, already four alternating quantifier blocks suffice for undecidability of $\alpha$-PA sentences.]]> 0 The Complexity of Reachability in Affine Vector Addition Systems with States Tue, 20 Jul 2021 06:28:35 +0000 https://doi.org/10.46298/lmcs-17(3:3)2021 https://doi.org/10.46298/lmcs-17(3:3)2021 Blondin, Michael Raskin, Mikhail Blondin, Michael Raskin, Mikhail 0 Affine Extensions of Integer Vector Addition Systems with States Tue, 20 Jul 2021 06:25:30 +0000 https://doi.org/10.46298/lmcs-17(3:1)2021 https://doi.org/10.46298/lmcs-17(3:1)2021 Blondin, Michael Haase, Christoph Mazowiecki, Filip Raskin, Mikhail Blondin, Michael Haase, Christoph Mazowiecki, Filip Raskin, Mikhail 0 Encoding many-valued logic in $\lambda$-calculus Tue, 29 Jun 2021 07:53:49 +0000 https://doi.org/10.46298/lmcs-17(2:25)2021 https://doi.org/10.46298/lmcs-17(2:25)2021 de Vries, Fer-Jan de Vries, Fer-Jan 0 Discovering ePassport Vulnerabilities using Bisimilarity Wed, 02 Jun 2021 14:00:18 +0000 https://doi.org/10.23638/LMCS-17(2:24)2021 https://doi.org/10.23638/LMCS-17(2:24)2021 Horne, Ross Mauw, Sjouke Horne, Ross Mauw, Sjouke 0 Algebraic cocompleteness and finitary functors Fri, 28 May 2021 06:35:52 +0000 https://doi.org/10.23638/LMCS-17(2:23)2021 https://doi.org/10.23638/LMCS-17(2:23)2021 Adámek, Jiří Adámek, Jiří 0 Predicative theories of continuous lattices Thu, 27 May 2021 07:12:04 +0000 https://doi.org/10.23638/LMCS-17(2:22)2021 https://doi.org/10.23638/LMCS-17(2:22)2021 Kawai, Tatsuji Kawai, Tatsuji 0 A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice Thu, 27 May 2021 07:06:45 +0000 https://doi.org/10.23638/LMCS-17(2:21)2021 https://doi.org/10.23638/LMCS-17(2:21)2021 Maietti, Maria Emilia Maschio, Samuele Rathjen, Michael Maietti, Maria Emilia Maschio, Samuele Rathjen, Michael 0 Star Games and Hydras Thu, 27 May 2021 06:58:01 +0000 https://doi.org/10.23638/LMCS-17(2:20)2021 https://doi.org/10.23638/LMCS-17(2:20)2021 Endrullis, Jörg Klop, Jan Willem Overbeek, Roy Endrullis, Jörg Klop, Jan Willem Overbeek, Roy 0 Interface Modeling for Quality and Resource Management Wed, 26 May 2021 07:59:59 +0000 https://doi.org/10.23638/LMCS-17(2:19)2021 https://doi.org/10.23638/LMCS-17(2:19)2021 Hendriks, Martijn Geilen, Marc Goossens, Kees de Jong, Rob Basten, Twan Hendriks, Martijn Geilen, Marc Goossens, Kees de Jong, Rob Basten, Twan 0 Theories of real addition with and without a predicate for integers Wed, 26 May 2021 07:59:28 +0000 https://doi.org/10.23638/LMCS-17(2:18)2021 https://doi.org/10.23638/LMCS-17(2:18)2021 Bès, Alexis Choffrut, Christian Bès, Alexis Choffrut, Christian 0 Presentable signatures and initial semantics Wed, 26 May 2021 07:59:01 +0000 https://doi.org/10.23638/LMCS-17(2:17)2021 https://doi.org/10.23638/LMCS-17(2:17)2021 Ahrens, Benedikt Hirschowitz, André Lafont, Ambroise Maggesi, Marco Ahrens, Benedikt Hirschowitz, André Lafont, Ambroise Maggesi, Marco 0 Computable analysis and notions of continuity in Coq Wed, 12 May 2021 20:59:39 +0000 https://doi.org/10.23638/LMCS-17(2:16)2021 https://doi.org/10.23638/LMCS-17(2:16)2021 Steinberg, Florian Thery, Laurent Thies, Holger Steinberg, Florian Thery, Laurent Thies, Holger 0 Partially Ordered Automata and Piecewise Testability Tue, 11 May 2021 12:57:11 +0000 https://doi.org/10.23638/LMCS-17(2:14)2021 https://doi.org/10.23638/LMCS-17(2:14)2021 Masopust, Tomáš Krötzsch, Markus Masopust, Tomáš Krötzsch, Markus 0 Decidability for Entailments of Symbolic Heaps with Arrays Tue, 11 May 2021 07:03:33 +0000 https://doi.org/10.23638/LMCS-17(2:15)2021 https://doi.org/10.23638/LMCS-17(2:15)2021 Kimura, Daisuke Tatsuta, Makoto Kimura, Daisuke Tatsuta, Makoto 0 Parametric updates in parametric timed automata Mon, 10 May 2021 13:36:28 +0000 https://doi.org/10.23638/LMCS-17(2:13)2021 https://doi.org/10.23638/LMCS-17(2:13)2021 André, Étienne Lime, Didier Ramparison, Mathias André, Étienne Lime, Didier Ramparison, Mathias 0 DRAT and Propagation Redundancy Proofs Without New Variables Fri, 23 Apr 2021 12:41:04 +0000 https://doi.org/10.23638/LMCS-17(2:12)2021 https://doi.org/10.23638/LMCS-17(2:12)2021 Buss, Sam Thapen, Neil Buss, Sam Thapen, Neil 0 Failure Trace Semantics for a Process Algebra with Time-outs Fri, 23 Apr 2021 06:49:10 +0000 https://doi.org/10.23638/LMCS-17(2:11)2021 https://doi.org/10.23638/LMCS-17(2:11)2021 van Glabbeek, Rob van Glabbeek, Rob 0 LNL-FPC: The Linear/Non-linear Fixpoint Calculus Thu, 22 Apr 2021 06:46:31 +0000 https://doi.org/10.23638/LMCS-17(2:9)2021 https://doi.org/10.23638/LMCS-17(2:9)2021 Lindenhovius, Bert Mislove, Michael Zamdzhiev, Vladimir Lindenhovius, Bert Mislove, Michael Zamdzhiev, Vladimir 0 Constructing Higher Inductive Types as Groupoid Quotients Thu, 22 Apr 2021 06:46:23 +0000 https://doi.org/10.23638/LMCS-17(2:8)2021 https://doi.org/10.23638/LMCS-17(2:8)2021 Veltri, Niccolò van der Weide, Niels Veltri, Niccolò van der Weide, Niels 0 Reachability Switching Games Thu, 22 Apr 2021 06:46:15 +0000 https://doi.org/10.23638/LMCS-17(2:10)2021 https://doi.org/10.23638/LMCS-17(2:10)2021 Fearnley, John Gairing, Martin Mnich, Matthias Savani, Rahul Fearnley, John Gairing, Martin Mnich, Matthias Savani, Rahul 0 Logic for exact real arithmetic Tue, 20 Apr 2021 05:55:27 +0000 https://doi.org/10.23638/LMCS-17(2:7)2021 https://doi.org/10.23638/LMCS-17(2:7)2021 Schwichtenberg, Helmut Wiesnet, Franziskus Schwichtenberg, Helmut Wiesnet, Franziskus 0 Algebraic Language Theory for Eilenberg--Moore Algebras Wed, 14 Apr 2021 11:52:56 +0000 https://doi.org/10.23638/LMCS-17(2:6)2021 https://doi.org/10.23638/LMCS-17(2:6)2021 Blumensath, Achim Blumensath, Achim 0 Sculptures in Concurrency Wed, 14 Apr 2021 11:52:53 +0000 https://doi.org/10.23638/LMCS-17(2:5)2021 https://doi.org/10.23638/LMCS-17(2:5)2021 Fahrenberg, Uli Johansen, Christian Trotter, Christopher A. Ziemiański, Krzysztof Fahrenberg, Uli Johansen, Christian Trotter, Christopher A. Ziemiański, Krzysztof 0 Direct spectra of Bishop spaces and their limits Wed, 14 Apr 2021 11:52:45 +0000 https://doi.org/10.23638/LMCS-17(2:4)2021 https://doi.org/10.23638/LMCS-17(2:4)2021 Petrakis, Iosif Petrakis, Iosif 0 Semipullbacks of labelled Markov processes Wed, 14 Apr 2021 11:52:38 +0000 https://doi.org/10.23638/LMCS-17(2:3)2021 https://doi.org/10.23638/LMCS-17(2:3)2021 Pachl, Jan Sánchez Terraf, Pedro Pachl, Jan Sánchez Terraf, Pedro 0 Coalgebraic Semantics for Probabilistic Logic Programming Mon, 12 Apr 2021 12:04:06 +0000 https://doi.org/10.23638/LMCS-17(2:2)2021 https://doi.org/10.23638/LMCS-17(2:2)2021 Gu, Tao Zanasi, Fabio Gu, Tao Zanasi, Fabio 0 Superposition for Lambda-Free Higher-Order Logic Mon, 12 Apr 2021 09:50:32 +0000 https://doi.org/10.23638/LMCS-17(2:1)2021 https://doi.org/10.23638/LMCS-17(2:1)2021 Bentkamp, Alexander Blanchette, Jasmin Cruanes, Simon Waldmann, Uwe Bentkamp, Alexander Blanchette, Jasmin Cruanes, Simon Waldmann, Uwe 0 Reconfiguration and Message Losses in Parameterized Broadcast Networks Thu, 18 Mar 2021 13:51:41 +0000 https://doi.org/10.23638/LMCS-17(1:23)2021 https://doi.org/10.23638/LMCS-17(1:23)2021 Bertrand, Nathalie Bouyer, Patricia Majumdar, Anirban Bertrand, Nathalie Bouyer, Patricia Majumdar, Anirban 0 Synthesis of Data Word Transducers Thu, 18 Mar 2021 13:49:24 +0000 https://doi.org/10.23638/LMCS-17(1:22)2021 https://doi.org/10.23638/LMCS-17(1:22)2021 Exibard, Léo Filiot, Emmanuel Reynier, Pierre-Alain Exibard, Léo Filiot, Emmanuel Reynier, Pierre-Alain 0 Stubborn Set Reduction for Two-Player Reachability Games Thu, 18 Mar 2021 13:47:06 +0000 https://doi.org/10.23638/LMCS-17(1:21)2021 https://doi.org/10.23638/LMCS-17(1:21)2021 Bønneland, Frederik Meyer Jensen, Peter Gjøl Larsen, Kim Guldstrand Muñiz, Marco Srba, Jiří Bønneland, Frederik Meyer Jensen, Peter Gjøl Larsen, Kim Guldstrand Muñiz, Marco Srba, Jiří 0 A Sound Algorithm for Asynchronous Session Subtyping and its Implementation Thu, 04 Mar 2021 07:12:11 +0000 https://doi.org/10.23638/LMCS-17(1:20)2021 https://doi.org/10.23638/LMCS-17(1:20)2021 Bravetti, Mario Carbone, Marco Lange, Julien Yoshida, Nobuko Zavattaro, Gianluigi Bravetti, Mario Carbone, Marco Lange, Julien Yoshida, Nobuko Zavattaro, Gianluigi 0 Complete Call-by-Value Calculi of Control Operators II: Strong Termination Tue, 02 Mar 2021 13:16:23 +0000 https://doi.org/10.23638/LMCS-17(1:18)2021 https://doi.org/10.23638/LMCS-17(1:18)2021 Hasegawa, Ryu Hasegawa, Ryu 0 Constructive Domains with Classical Witnesses Tue, 02 Mar 2021 07:24:24 +0000 https://doi.org/10.23638/LMCS-17(1:19)2021 https://doi.org/10.23638/LMCS-17(1:19)2021 Pattinson, Dirk Mohammadian, Mina Pattinson, Dirk Mohammadian, Mina 0 Datatype defining rewrite systems for naturals and integers Thu, 18 Feb 2021 06:11:42 +0000 https://doi.org/10.23638/LMCS-17(1:17)2021 https://doi.org/10.23638/LMCS-17(1:17)2021 Bergstra, Jan A. Ponse, Alban Bergstra, Jan A. Ponse, Alban 0 A Formal Proof of the Irrationality of $\zeta(3)$ Thu, 18 Feb 2021 06:11:24 +0000 https://doi.org/10.23638/LMCS-17(1:16)2021 https://doi.org/10.23638/LMCS-17(1:16)2021 Mahboubi, Assia Sibut-Pinote, Thomas Mahboubi, Assia Sibut-Pinote, Thomas 0 Output-sensitive Information flow analysis Fri, 12 Feb 2021 06:50:28 +0000 https://doi.org/10.23638/LMCS-17(1:15)2021 https://doi.org/10.23638/LMCS-17(1:15)2021 Ene, Cristian Mounier, Laurent Potet, Marie-Laure Ene, Cristian Mounier, Laurent Potet, Marie-Laure 0 The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely Executable Wed, 10 Feb 2021 07:10:29 +0000 https://doi.org/10.23638/LMCS-17(1:14)2021 https://doi.org/10.23638/LMCS-17(1:14)2021 Luttik, Bas Yang, Fei Luttik, Bas Yang, Fei 0 Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras Tue, 09 Feb 2021 12:29:47 +0000 https://doi.org/10.23638/LMCS-17(1:13)2021 https://doi.org/10.23638/LMCS-17(1:13)2021 Dongol, Brijesh Hayes, Ian J. Struth, Georg Dongol, Brijesh Hayes, Ian J. Struth, Georg 0 Axiomatization of betweenness in order-theoretic trees Wed, 03 Feb 2021 08:58:45 +0000 https://doi.org/10.23638/LMCS-17(1:11)2021 https://doi.org/10.23638/LMCS-17(1:11)2021 Courcelle, Bruno Courcelle, Bruno 0 Robustness Against Transactional Causal Consistency Wed, 03 Feb 2021 08:54:42 +0000 https://doi.org/10.23638/LMCS-17(1:12)2021 https://doi.org/10.23638/LMCS-17(1:12)2021 Beillahi, Sidi Mohamed Bouajjani, Ahmed Enea, Constantin Beillahi, Sidi Mohamed Bouajjani, Ahmed Enea, Constantin 0 Determinacy in Discrete-Bidding Infinite-Duration Games Wed, 03 Feb 2021 08:53:13 +0000 https://doi.org/10.23638/LMCS-17(1:10)2021 https://doi.org/10.23638/LMCS-17(1:10)2021 Aghajohari, Milad Avni, Guy Henzinger, Thomas A. Aghajohari, Milad Avni, Guy Henzinger, Thomas A. 0 Computing Probabilistic Bisimilarity Distances for Probabilistic Automata Tue, 02 Feb 2021 22:51:57 +0000 https://doi.org/10.23638/LMCS-17(1:9)2021 https://doi.org/10.23638/LMCS-17(1:9)2021 Bacci, Giorgio Bacci, Giovanni Larsen, Kim G. Mardare, Radu Tang, Qiyi van Breugel, Franck Bacci, Giorgio Bacci, Giovanni Larsen, Kim G. Mardare, Radu Tang, Qiyi van Breugel, Franck 0 Correct and Efficient Antichain Algorithms for Refinement Checking Mon, 01 Feb 2021 12:19:43 +0000 https://doi.org/10.23638/LMCS-17(1:8)2021 https://doi.org/10.23638/LMCS-17(1:8)2021 Laveaux, Maurice Groote, Jan Friso Willemse, Tim A. C. Laveaux, Maurice Groote, Jan Friso Willemse, Tim A. C. 0 Solvability = Typability + Inhabitation Fri, 29 Jan 2021 10:20:07 +0000 https://doi.org/10.23638/LMCS-17(1:7)2021 https://doi.org/10.23638/LMCS-17(1:7)2021 Bucciarelli, Antonio Kesner, Delia Della Rocca, Simona Ronchi Bucciarelli, Antonio Kesner, Delia Della Rocca, Simona Ronchi 0 Modal Logics for Nominal Transition Systems Thu, 28 Jan 2021 11:40:19 +0000 https://doi.org/10.23638/LMCS-17(1:6)2021 https://doi.org/10.23638/LMCS-17(1:6)2021 Parrow, Joachim Borgström, Johannes Eriksson, Lars-Henrik Gutkovas, Ramūnas Forsberg Weber, Tjark Parrow, Joachim Borgström, Johannes Eriksson, Lars-Henrik Gutkovas, Ramūnas Forsberg Weber, Tjark 0 Definable decompositions for graphs of bounded linear cliquewidth Mon, 25 Jan 2021 11:13:48 +0000 https://doi.org/10.23638/LMCS-17(1:5)2021 https://doi.org/10.23638/LMCS-17(1:5)2021 Bojańczyk, Mikołaj Grohe, Martin Pilipczuk, Michał Bojańczyk, Mikołaj Grohe, Martin Pilipczuk, Michał 0 2-adjoint equivalences in homotopy type theory Fri, 22 Jan 2021 08:59:34 +0000 https://doi.org/10.23638/LMCS-17(1:3)2021 https://doi.org/10.23638/LMCS-17(1:3)2021 Carranza, Daniel Chang, Jonathan Kapulkin, Chris Sandford, Ryan Carranza, Daniel Chang, Jonathan Kapulkin, Chris Sandford, Ryan 0 Tameness in least fixed-point logic and McColm's conjecture Fri, 22 Jan 2021 08:55:55 +0000 https://doi.org/10.23638/LMCS-17(1:2)2021 https://doi.org/10.23638/LMCS-17(1:2)2021 Bhaskar, Siddharth Kruckman, Alex Bhaskar, Siddharth Kruckman, Alex 0 On the Strong Equivalences for LPMLN Programs Fri, 22 Jan 2021 08:52:14 +0000 https://doi.org/10.23638/LMCS-17(1:4)2021 https://doi.org/10.23638/LMCS-17(1:4)2021 Wang, Bin Shen, Jun Zhang, Shutao Zhang, Zhizheng Wang, Bin Shen, Jun Zhang, Shutao Zhang, Zhizheng 0 Axiomatizing Maximal Progress and Discrete Time Thu, 21 Jan 2021 07:54:29 +0000 https://doi.org/10.23638/LMCS-17(1:1)2021 https://doi.org/10.23638/LMCS-17(1:1)2021 Bravetti, Mario Bravetti, Mario 0 Towards a Minimal Stabilizer ZX-calculus Tue, 22 Dec 2020 08:46:24 +0000 https://doi.org/10.23638/LMCS-16(4:19)2020 https://doi.org/10.23638/LMCS-16(4:19)2020 Backens, Miriam Perdrix, Simon Wang, Quanlong Backens, Miriam Perdrix, Simon Wang, Quanlong 0 On open well-filtered spaces Fri, 18 Dec 2020 09:32:31 +0000 https://doi.org/10.23638/LMCS-16(4:18)2020 https://doi.org/10.23638/LMCS-16(4:18)2020 Shen, Chong Xi, Xiaoyong Xu, Xiaoquan Zhao, Dongsheng Shen, Chong Xi, Xiaoyong Xu, Xiaoquan Zhao, Dongsheng 0 Psi-Calculi Revisited: Connectivity and Compositionality Tue, 15 Dec 2020 07:05:44 +0000 https://doi.org/10.23638/LMCS-16(4:16)2020 https://doi.org/10.23638/LMCS-16(4:16)2020 Pohjola, Johannes Åman Pohjola, Johannes Åman 0 Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory Tue, 15 Dec 2020 07:02:38 +0000 https://doi.org/10.23638/LMCS-16(4:17)2020 https://doi.org/10.23638/LMCS-16(4:17)2020 Mannaa, Bassel Møgelberg, Rasmus Ejlers Veltri, Niccolò Mannaa, Bassel Møgelberg, Rasmus Ejlers Veltri, Niccolò 0 Towards Races in Linear Logic Tue, 15 Dec 2020 07:00:02 +0000 https://doi.org/10.23638/LMCS-16(4:15)2020 https://doi.org/10.23638/LMCS-16(4:15)2020 Kokke, Wen Morris, J. Garrett Wadler, Philip Kokke, Wen Morris, J. Garrett Wadler, Philip 0 Life is Random, Time is Not: Markov Decision Processes with Window Objectives Mon, 14 Dec 2020 14:08:49 +0000 https://doi.org/10.23638/LMCS-16(4:13)2020 https://doi.org/10.23638/LMCS-16(4:13)2020 Brihaye, Thomas Delgrange, Florent Oualhadj, Youssouf Randour, Mickael Brihaye, Thomas Delgrange, Florent Oualhadj, Youssouf Randour, Mickael 0 Theory of higher order interpretations and application to Basic Feasible Functions Mon, 14 Dec 2020 11:10:47 +0000 https://doi.org/10.23638/LMCS-16(4:14)2020 https://doi.org/10.23638/LMCS-16(4:14)2020 Hainry, Emmanuel Péchoux, Romain Hainry, Emmanuel Péchoux, Romain 0 An extended type system with lambda-typed lambda-expressions Tue, 01 Dec 2020 13:44:45 +0000 https://doi.org/10.23638/LMCS-16(4:12)2020 https://doi.org/10.23638/LMCS-16(4:12)2020 Weber, Matthias Weber, Matthias 0 Clause Set Cycles and Induction Mon, 30 Nov 2020 07:31:51 +0000 https://doi.org/10.23638/LMCS-16(4:11)2020 https://doi.org/10.23638/LMCS-16(4:11)2020 Hetzl, Stefan Vierling, Jannik Hetzl, Stefan Vierling, Jannik 0 Convexity and Order in Probabilistic Call-by-Name FPC Thu, 12 Nov 2020 22:16:41 +0000 https://doi.org/10.23638/LMCS-16(4:10)2020 https://doi.org/10.23638/LMCS-16(4:10)2020 Rennela, Mathys Rennela, Mathys 0 Transfinite Lyndon words Tue, 10 Nov 2020 13:24:14 +0000 https://doi.org/10.23638/LMCS-16(4:9)2020 https://doi.org/10.23638/LMCS-16(4:9)2020 Carton, Olivier Boasson, Luc Carton, Olivier Boasson, Luc 0 The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games Thu, 05 Nov 2020 22:27:54 +0000 https://doi.org/10.23638/LMCS-16(4:8)2020 https://doi.org/10.23638/LMCS-16(4:8)2020 Brihaye, Thomas Bruyère, Véronique Goeminne, Aline Raskin, Jean-François Bogaard, Marie van den Brihaye, Thomas Bruyère, Véronique Goeminne, Aline Raskin, Jean-François Bogaard, Marie van den 0 Collaboration vs. choreography conformance in BPMN Tue, 27 Oct 2020 18:25:49 +0000 https://doi.org/10.23638/LMCS-16(4:7)2020 https://doi.org/10.23638/LMCS-16(4:7)2020 Corradini, Flavio Morichetta, Andrea Polini, Andrea Re, Barbara Tiezzi, Francesco Corradini, Flavio Morichetta, Andrea Polini, Andrea Re, Barbara Tiezzi, Francesco 0 A Functional (Monadic) Second-Order Theory of Infinite Trees Fri, 23 Oct 2020 07:21:11 +0000 https://doi.org/10.23638/LMCS-16(4:6)2020 https://doi.org/10.23638/LMCS-16(4:6)2020 Das, Anupam Riba, Colin Das, Anupam Riba, Colin 0 Reversing Place Transition Nets Fri, 16 Oct 2020 06:56:37 +0000 https://doi.org/10.23638/LMCS-16(4:5)2020 https://doi.org/10.23638/LMCS-16(4:5)2020 Melgratti, Hernán Mezzina, Claudio Antares Ulidowski, Irek Melgratti, Hernán Mezzina, Claudio Antares Ulidowski, Irek 0 Verification of Flat FIFO Systems Wed, 14 Oct 2020 12:27:24 +0000 https://doi.org/10.23638/LMCS-16(4:4)2020 https://doi.org/10.23638/LMCS-16(4:4)2020 Finkel, Alain Praveen, M. Finkel, Alain Praveen, M. 0 Of Cores: A Partial-Exploration Framework for Markov Decision Processes Fri, 09 Oct 2020 07:12:19 +0000 https://doi.org/10.23638/LMCS-16(4:3)2020 https://doi.org/10.23638/LMCS-16(4:3)2020 Křetínský, Jan Meggendorfer, Tobias Křetínský, Jan Meggendorfer, Tobias 0 On the Termination Problem for Probabilistic Higher-Order Recursive Programs Fri, 02 Oct 2020 06:39:59 +0000 https://doi.org/10.23638/LMCS-16(4:2)2020 https://doi.org/10.23638/LMCS-16(4:2)2020 Kobayashi, Naoki Lago, Ugo Dal Grellois, Charles Kobayashi, Naoki Lago, Ugo Dal Grellois, Charles 0 Field-based Coordination with the Share Operator Fri, 02 Oct 2020 06:37:11 +0000 https://doi.org/10.23638/LMCS-16(4:1)2020 https://doi.org/10.23638/LMCS-16(4:1)2020 Audrito, Giorgio Beal, Jacob Damiani, Ferruccio Pianini, Danilo Viroli, Mirko Audrito, Giorgio Beal, Jacob Damiani, Ferruccio Pianini, Danilo Viroli, Mirko 0 A symmetric protocol to establish service level agreements Wed, 30 Sep 2020 13:06:52 +0000 https://doi.org/10.23638/LMCS-16(3:19)2020 https://doi.org/10.23638/LMCS-16(3:19)2020 Groote, Jan Friso Willemse, Tim A. C. Groote, Jan Friso Willemse, Tim A. C. 0 On Resolving Non-determinism in Choreographies Thu, 24 Sep 2020 13:08:33 +0000 https://doi.org/10.23638/LMCS-16(3:18)2020 https://doi.org/10.23638/LMCS-16(3:18)2020 Bocchi, Laura Melgratti, Hernan Tuosto, Emilio Bocchi, Laura Melgratti, Hernan Tuosto, Emilio 0 A unifying framework for continuity and complexity in higher types Wed, 09 Sep 2020 07:01:51 +0000 https://doi.org/10.23638/LMCS-16(3:17)2020 https://doi.org/10.23638/LMCS-16(3:17)2020 Powell, Thomas Powell, Thomas 0 Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership Tue, 08 Sep 2020 12:13:07 +0000 https://doi.org/10.23638/LMCS-16(3:16)2020 https://doi.org/10.23638/LMCS-16(3:16)2020 Krebs, Andreas Lodaya, Kamal Pandya, Paritosh K. Straubing, Howard Krebs, Andreas Lodaya, Kamal Pandya, Paritosh K. Straubing, Howard 0 Gems of Corrado Böhm Wed, 02 Sep 2020 14:24:39 +0000 https://doi.org/10.23638/LMCS-16(3:15)2020 https://doi.org/10.23638/LMCS-16(3:15)2020 Barendregt, Henk P. Barendregt, Henk P. 0 Rooted Divergence-Preserving Branching Bisimilarity is a Congruence Fri, 28 Aug 2020 06:54:32 +0000 https://doi.org/10.23638/LMCS-16(3:14)2020 https://doi.org/10.23638/LMCS-16(3:14)2020 van Glabbeek, Rob Luttik, Bas Spaninks, Linda van Glabbeek, Rob Luttik, Bas Spaninks, Linda 0 Compiling With Classical Connectives Fri, 28 Aug 2020 06:50:35 +0000 https://doi.org/10.23638/LMCS-16(3:13)2020 https://doi.org/10.23638/LMCS-16(3:13)2020 Downen, Paul Ariola, Zena M. Downen, Paul Ariola, Zena M. 0 The Sierpinski Object in the Scott Realizability Topos Thu, 20 Aug 2020 07:29:03 +0000 https://doi.org/10.23638/LMCS-16(3:12)2020 https://doi.org/10.23638/LMCS-16(3:12)2020 de Jong, Tom van Oosten, Jaap de Jong, Tom van Oosten, Jaap 0 On the Expressive Power of Higher-Order Pushdown Systems Thu, 20 Aug 2020 07:25:44 +0000 https://doi.org/10.23638/LMCS-16(3:11)2020 https://doi.org/10.23638/LMCS-16(3:11)2020 Parys, Paweł Parys, Paweł 0 Dual-Context Calculi for Modal Logic Wed, 19 Aug 2020 13:58:19 +0000 https://doi.org/10.23638/LMCS-16(3:10)2020 https://doi.org/10.23638/LMCS-16(3:10)2020 Kavvos, G. A. Kavvos, G. A. 0 A limitation on the KPT interpolation Wed, 12 Aug 2020 07:46:56 +0000 https://doi.org/10.23638/LMCS-16(3:9)2020 https://doi.org/10.23638/LMCS-16(3:9)2020 Krajíček, Jan Krajíček, Jan 0 Constructive Canonicity of Inductive Inequalities Wed, 05 Aug 2020 08:42:23 +0000 https://doi.org/10.23638/LMCS-16(3:8)2020 https://doi.org/10.23638/LMCS-16(3:8)2020 Conradie, Willem Palmigiano, Alessandra Conradie, Willem Palmigiano, Alessandra 0 Fixed point combinators as fixed points of higher-order fixed point generators Thu, 23 Jul 2020 08:55:05 +0000 https://doi.org/10.23638/LMCS-16(3:7)2020 https://doi.org/10.23638/LMCS-16(3:7)2020 Polonsky, Andrew Polonsky, Andrew 0 Revisiting Call-by-value Böhm trees in light of their Taylor expansion Wed, 15 Jul 2020 06:36:26 +0000 https://doi.org/10.23638/LMCS-16(3:6)2020 https://doi.org/10.23638/LMCS-16(3:6)2020 Kerinec, Emma Manzonetto, Giulio Pagani, Michele Kerinec, Emma Manzonetto, Giulio Pagani, Michele 0 Interpolating Between Choices for the Approximate Intermediate Value Theorem Tue, 14 Jul 2020 06:33:57 +0000 https://doi.org/10.23638/LMCS-16(3:5)2020 https://doi.org/10.23638/LMCS-16(3:5)2020 Frank, Matthew Frank, Matthew 0 Directed Homotopy in Non-Positively Curved Spaces Mon, 13 Jul 2020 07:45:58 +0000 https://doi.org/10.23638/LMCS-16(3:4)2020 https://doi.org/10.23638/LMCS-16(3:4)2020 Goubault, Eric Mimram, Samuel Goubault, Eric Mimram, Samuel 0 Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems Fri, 10 Jul 2020 09:42:39 +0000 https://doi.org/10.23638/LMCS-16(3:3)2020 https://doi.org/10.23638/LMCS-16(3:3)2020 Behr, Nicolas Danos, Vincent Garnier, Ilias Behr, Nicolas Danos, Vincent Garnier, Ilias 0 Rule Algebras for Adhesive Categories Fri, 03 Jul 2020 07:47:09 +0000 https://doi.org/10.23638/LMCS-16(3:2)2020 https://doi.org/10.23638/LMCS-16(3:2)2020 Behr, Nicolas Sobocinski, Pawel Behr, Nicolas Sobocinski, Pawel 0 Playing with Repetitions in Data Words Using Energy Games Fri, 03 Jul 2020 07:44:27 +0000 https://doi.org/10.23638/LMCS-16(3:1)2020 https://doi.org/10.23638/LMCS-16(3:1)2020 Figueira, Diego Majumdar, Anirban Praveen, M. Figueira, Diego Majumdar, Anirban Praveen, M. 0 Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality Tue, 30 Jun 2020 08:52:41 +0000 https://doi.org/10.23638/LMCS-16(2:14)2020 https://doi.org/10.23638/LMCS-16(2:14)2020 Abel, Andreas Coquand, Thierry Abel, Andreas Coquand, Thierry 0 Forward Analysis for WSTS, Part III: Karp-Miller Trees Tue, 23 Jun 2020 06:55:18 +0000 https://doi.org/10.23638/LMCS-16(2:13)2020 https://doi.org/10.23638/LMCS-16(2:13)2020 Blondin, Michael Finkel, Alain Goubault-Larrecq, Jean Blondin, Michael Finkel, Alain Goubault-Larrecq, Jean 0 Consistency of circuit lower bounds with bounded theories Thu, 18 Jun 2020 09:49:26 +0000 https://doi.org/10.23638/LMCS-16(2:12)2020 https://doi.org/10.23638/LMCS-16(2:12)2020 Bydzovsky, Jan Krajicek, Jan Oliveira, Igor C. Bydzovsky, Jan Krajicek, Jan Oliveira, Igor C. 0 Completeness of the ZX-Calculus Thu, 04 Jun 2020 08:42:58 +0000 https://doi.org/10.23638/LMCS-16(2:11)2020 https://doi.org/10.23638/LMCS-16(2:11)2020 Jeandel, Emmanuel Perdrix, Simon Vilmart, Renaud Jeandel, Emmanuel Perdrix, Simon Vilmart, Renaud 0 Trace Refinement in Labelled Markov Decision Processes Wed, 03 Jun 2020 07:45:10 +0000 https://doi.org/10.23638/LMCS-16(2:10)2020 https://doi.org/10.23638/LMCS-16(2:10)2020 Fijalkow, Nathanaël Kiefer, Stefan Shirmohammadi, Mahsa Fijalkow, Nathanaël Kiefer, Stefan Shirmohammadi, Mahsa 0 Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services Wed, 03 Jun 2020 07:38:35 +0000 https://doi.org/10.23638/LMCS-16(2:9)2020 https://doi.org/10.23638/LMCS-16(2:9)2020 Basile, Davide ter Beek, Maurice H. Pugliese, Rosario Basile, Davide ter Beek, Maurice H. Pugliese, Rosario 0 On properties of $B$-terms Tue, 02 Jun 2020 07:56:01 +0000 https://doi.org/10.23638/LMCS-16(2:8)2020 https://doi.org/10.23638/LMCS-16(2:8)2020 Ikebuchi, Mirai Nakano, Keisuke Ikebuchi, Mirai Nakano, Keisuke 0 Cellular Cohomology in Homotopy Type Theory Mon, 01 Jun 2020 09:26:52 +0000 https://doi.org/10.23638/LMCS-16(2:7)2020 https://doi.org/10.23638/LMCS-16(2:7)2020 Buchholtz, Ulrik Hou, Kuen-Bang Buchholtz, Ulrik Hou, Kuen-Bang 0 Register Games Tue, 19 May 2020 08:45:39 +0000 https://doi.org/10.23638/LMCS-16(2:6)2020 https://doi.org/10.23638/LMCS-16(2:6)2020 Lehtinen, Karoliina Boker, Udi Lehtinen, Karoliina Boker, Udi 0 Tight Polynomial Worst-Case Bounds for Loop Programs Thu, 14 May 2020 07:39:28 +0000 https://doi.org/10.23638/LMCS-16(2:4)2020 https://doi.org/10.23638/LMCS-16(2:4)2020 Ben-Amram, Amir M. Hamilton, Geoff Ben-Amram, Amir M. Hamilton, Geoff 0 On the incomputability of computable dimension Thu, 14 May 2020 06:08:42 +0000 https://doi.org/10.23638/LMCS-16(2:5)2020 https://doi.org/10.23638/LMCS-16(2:5)2020 Staiger, Ludwig Staiger, Ludwig 0 Representing Dependencies in Event Structures Wed, 13 May 2020 07:30:09 +0000 https://doi.org/10.23638/LMCS-16(2:3)2020 https://doi.org/10.23638/LMCS-16(2:3)2020 Pinna, G. Michele Pinna, G. Michele 0 Reachability for infinite time Turing machines with long tapes Fri, 24 Apr 2020 10:37:30 +0000 https://doi.org/10.23638/LMCS-16(2:2)2020 https://doi.org/10.23638/LMCS-16(2:2)2020 Carl, Merlin Rin, Benjamin Schlicht, Philipp Carl, Merlin Rin, Benjamin Schlicht, Philipp 0 An Integrated First-Order Theory of Points and Intervals over Linear Orders (Part II) Wed, 01 Apr 2020 10:53:37 +0000 https://doi.org/10.23638/LMCS-16(2:1)2020 https://doi.org/10.23638/LMCS-16(2:1)2020 Conradie, Willem Durhan, Salih Sciavicco, Guido Conradie, Willem Durhan, Salih Sciavicco, Guido 0 Automata Minimization: a Functorial Approach Mon, 23 Mar 2020 09:51:00 +0000 https://doi.org/10.23638/LMCS-16(1:32)2020 https://doi.org/10.23638/LMCS-16(1:32)2020 Colcombet, Thomas Petrişan, Daniela Colcombet, Thomas Petrişan, Daniela 0 A new coinductive confluence proof for infinitary lambda calculus Wed, 11 Mar 2020 08:23:19 +0000 https://doi.org/10.23638/LMCS-16(1:31)2020 https://doi.org/10.23638/LMCS-16(1:31)2020 Czajka, Łukasz Czajka, Łukasz 0 Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory Tue, 10 Mar 2020 17:57:09 +0000 https://doi.org/10.23638/LMCS-16(1:30)2020 https://doi.org/10.23638/LMCS-16(1:30)2020 Rennela, Mathys Staton, Sam Rennela, Mathys Staton, Sam 0 Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems Mon, 02 Mar 2020 08:32:54 +0000 https://doi.org/10.23638/LMCS-16(1:29)2020 https://doi.org/10.23638/LMCS-16(1:29)2020 Semenov, Alexander Otpuschennikov, Ilya Gribanova, Irina Zaikin, Oleg Kochemazov, Stepan Semenov, Alexander Otpuschennikov, Ilya Gribanova, Irina Zaikin, Oleg Kochemazov, Stepan 0 Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix Fri, 28 Feb 2020 09:24:20 +0000 https://doi.org/10.23638/LMCS-16(1:27)2020 https://doi.org/10.23638/LMCS-16(1:27)2020 Nguyên, Lê Thành Dũng Nguyên, Lê Thành Dũng 0 A Universal Ordinary Differential Equation Fri, 28 Feb 2020 07:37:16 +0000 https://doi.org/10.23638/LMCS-16(1:28)2020 https://doi.org/10.23638/LMCS-16(1:28)2020 Bournez, Olivier Pouly, Amaury Bournez, Olivier Pouly, Amaury 0 First-order queries on classes of structures with bounded expansion Tue, 25 Feb 2020 14:07:34 +0000 https://doi.org/10.23638/LMCS-16(1:25)2020 https://doi.org/10.23638/LMCS-16(1:25)2020 Kazana, Wojtek Segoufin, Luc Kazana, Wojtek Segoufin, Luc 0 Distances between States and between Predicates Tue, 25 Feb 2020 08:44:28 +0000 https://doi.org/10.23638/LMCS-16(1:26)2020 https://doi.org/10.23638/LMCS-16(1:26)2020 Jacobs, Bart Westerbaan, Abraham Jacobs, Bart Westerbaan, Abraham 0 Continuity of Functional Transducers: A Profinite Study of Rational Functions Fri, 21 Feb 2020 09:47:52 +0000 https://doi.org/10.23638/LMCS-16(1:24)2020 https://doi.org/10.23638/LMCS-16(1:24)2020 Cadilhac, Michaël Carton, Olivier Paperman, Charles Cadilhac, Michaël Carton, Olivier Paperman, Charles 0 Decreasing Diagrams for Confluence and Commutation Thu, 20 Feb 2020 17:52:49 +0000 https://doi.org/10.23638/LMCS-16(1:23)2020 https://doi.org/10.23638/LMCS-16(1:23)2020 Endrullis, Jörg Klop, Jan Willem Overbeek, Roy Endrullis, Jörg Klop, Jan Willem Overbeek, Roy 0 A syntactic approach to continuity of T-definable functionals Thu, 20 Feb 2020 17:46:34 +0000 https://doi.org/10.23638/LMCS-16(1:22)2020 https://doi.org/10.23638/LMCS-16(1:22)2020 Xu, Chuangjie Xu, Chuangjie 0 The Complexity of Combinations of Qualitative Constraint Satisfaction Problems Thu, 20 Feb 2020 17:21:54 +0000 https://doi.org/10.23638/LMCS-16(1:21)2020 https://doi.org/10.23638/LMCS-16(1:21)2020 Bodirsky, Manuel Greiner, Johannes Bodirsky, Manuel Greiner, Johannes 0 Coaxioms: flexible coinductive definitions by inference systems Thu, 20 Feb 2020 09:42:42 +0000 https://doi.org/10.23638/LMCS-15(1:26)2019 https://doi.org/10.23638/LMCS-15(1:26)2019 Dagnino, Francesco Dagnino, Francesco 0 Recursion Schemes, the MSO Logic, and the U quantifier Tue, 18 Feb 2020 09:47:38 +0000 https://doi.org/10.23638/LMCS-16(1:20)2020 https://doi.org/10.23638/LMCS-16(1:20)2020 Parys, Paweł Parys, Paweł 0 On Nominal Syntax and Permutation Fixed Points Mon, 17 Feb 2020 06:43:58 +0000 https://doi.org/10.23638/LMCS-16(1:19)2020 https://doi.org/10.23638/LMCS-16(1:19)2020 Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele 0 McShane-Whitney extensions in constructive analysis Mon, 17 Feb 2020 06:07:51 +0000 https://doi.org/10.23638/LMCS-16(1:18)2020 https://doi.org/10.23638/LMCS-16(1:18)2020 Petrakis, Iosif Petrakis, Iosif 0 Continuous Regular Functions Fri, 14 Feb 2020 09:43:46 +0000 https://doi.org/10.23638/LMCS-16(1:17)2020 https://doi.org/10.23638/LMCS-16(1:17)2020 Gorman, Alexi Block Hieronymi, Philipp Kaplan, Elliot Meng, Ruoyu Walsberg, Erik Wang, Zihe Xiong, Ziqin Yang, Hongru Gorman, Alexi Block Hieronymi, Philipp Kaplan, Elliot Meng, Ruoyu Walsberg, Erik Wang, Zihe Xiong, Ziqin Yang, Hongru 0 Regular Tree Algebras Thu, 13 Feb 2020 09:59:30 +0000 https://doi.org/10.23638/LMCS-16(1:16)2020 https://doi.org/10.23638/LMCS-16(1:16)2020 Blumensath, Achim Blumensath, Achim 0 Signatures and Induction Principles for Higher Inductive-Inductive Types Thu, 13 Feb 2020 09:57:31 +0000 https://doi.org/10.23638/LMCS-16(1:10)2020 https://doi.org/10.23638/LMCS-16(1:10)2020 Kaposi, Ambrus Kovács, András Kaposi, Ambrus Kovács, András 0 Minimization of visibly pushdown automata is NP-complete Thu, 13 Feb 2020 09:57:00 +0000 https://doi.org/10.23638/LMCS-16(1:14)2020 https://doi.org/10.23638/LMCS-16(1:14)2020 Gauwin, Olivier Muscholl, Anca Raskin, Michael Gauwin, Olivier Muscholl, Anca Raskin, Michael 0 An operational interpretation of coinductive types Thu, 13 Feb 2020 09:53:46 +0000 https://doi.org/10.23638/LMCS-16(1:11)2020 https://doi.org/10.23638/LMCS-16(1:11)2020 Czajka, Łukasz Czajka, Łukasz 0 Overlap Algebras: a Constructive Look at Complete Boolean Algebras Thu, 13 Feb 2020 08:16:38 +0000 https://doi.org/10.23638/LMCS-16(1:13)2020 https://doi.org/10.23638/LMCS-16(1:13)2020 Ciraulo, Francesco Contente, Michele Ciraulo, Francesco Contente, Michele 0 Undecidability of a weak version of MSO+U Tue, 11 Feb 2020 09:01:06 +0000 https://doi.org/10.23638/LMCS-16(1:12)2020 https://doi.org/10.23638/LMCS-16(1:12)2020 Bojańczyk, Mikołaj Daviaud, Laure Guillon, Bruno Penelle, Vincent Sreejith, A. V. Bojańczyk, Mikołaj Daviaud, Laure Guillon, Bruno Penelle, Vincent Sreejith, A. V. 0 Descriptive Complexity for Counting Complexity Classes Mon, 10 Feb 2020 10:17:48 +0000 https://doi.org/10.23638/LMCS-16(1:9)2020 https://doi.org/10.23638/LMCS-16(1:9)2020 Arenas, Marcelo Muñoz, Martin Riveros, Cristian Arenas, Marcelo Muñoz, Martin Riveros, Cristian 0 Efficient and Modular Coalgebraic Partition Refinement Fri, 31 Jan 2020 12:48:55 +0000 https://doi.org/10.23638/LMCS-16(1:8)2020 https://doi.org/10.23638/LMCS-16(1:8)2020 Wißmann, Thorsten Dorsch, Ulrich Milius, Stefan Schröder, Lutz Wißmann, Thorsten Dorsch, Ulrich Milius, Stefan Schröder, Lutz 0 Call-by-name Gradual Type Theory Fri, 31 Jan 2020 07:48:12 +0000 https://doi.org/10.23638/LMCS-16(1:7)2020 https://doi.org/10.23638/LMCS-16(1:7)2020 New, Max S. Licata, Daniel R. New, Max S. Licata, Daniel R. 0 Probabilistic logics based on Riesz spaces Mon, 27 Jan 2020 11:44:09 +0000 https://doi.org/10.23638/LMCS-16(1:6)2020 https://doi.org/10.23638/LMCS-16(1:6)2020 Furber, Robert Mardare, Radu Mio, Matteo Furber, Robert Mardare, Radu Mio, Matteo 0 Language Preservation Problems in Parametric Timed Automata Wed, 22 Jan 2020 08:03:05 +0000 https://doi.org/10.23638/LMCS-16(1:5)2020 https://doi.org/10.23638/LMCS-16(1:5)2020 André, Étienne Lime, Didier Markey, Nicolas André, Étienne Lime, Didier Markey, Nicolas 0 A Categorical Reconstruction of Quantum Theory Fri, 17 Jan 2020 08:13:55 +0000 https://doi.org/10.23638/LMCS-16(1:4)2020 https://doi.org/10.23638/LMCS-16(1:4)2020 Tull, Sean Tull, Sean 0 Non-idempotent types for classical calculi in natural deduction style Tue, 14 Jan 2020 12:25:09 +0000 https://doi.org/10.23638/LMCS-16(1:3)2020 https://doi.org/10.23638/LMCS-16(1:3)2020 Kesner, Delia Vial, Pierre Kesner, Delia Vial, Pierre 0 Modalities in homotopy type theory Wed, 08 Jan 2020 09:14:13 +0000 https://doi.org/10.23638/LMCS-16(1:2)2020 https://doi.org/10.23638/LMCS-16(1:2)2020 Rijke, Egbert Shulman, Michael Spitters, Bas Rijke, Egbert Shulman, Michael Spitters, Bas 0 On the logical complexity of cyclic arithmetic Mon, 06 Jan 2020 15:29:31 +0000 https://doi.org/10.23638/LMCS-16(1:1)2020 https://doi.org/10.23638/LMCS-16(1:1)2020 Das, Anupam Das, Anupam 0 Concurrency and Probability: Removing Confusion, Compositionally Thu, 19 Dec 2019 10:38:20 +0000 https://doi.org/10.23638/LMCS-15(4:17)2019 https://doi.org/10.23638/LMCS-15(4:17)2019 Bruni, Roberto Melgratti, Hernán Montanari, Ugo Bruni, Roberto Melgratti, Hernán Montanari, Ugo 0 Relational $\star$-Liftings for Differential Privacy Thu, 19 Dec 2019 08:49:10 +0000 https://doi.org/10.23638/LMCS-15(4:18)2019 https://doi.org/10.23638/LMCS-15(4:18)2019 Barthe, Gilles Espitau, Thomas Hsu, Justin Sato, Tetsuya Strub, Pierre-Yves Barthe, Gilles Espitau, Thomas Hsu, Justin Sato, Tetsuya Strub, Pierre-Yves 0 Logical and Algebraic Characterizations of Rational Transductions Thu, 19 Dec 2019 08:26:34 +0000 https://doi.org/10.23638/LMCS-15(4:16)2019 https://doi.org/10.23638/LMCS-15(4:16)2019 Filiot, Emmanuel Gauwin, Olivier Lhote, Nathan Filiot, Emmanuel Gauwin, Olivier Lhote, Nathan 0 On Functions Weakly Computable by Pushdown Petri Nets and Related Systems Wed, 18 Dec 2019 08:30:05 +0000 https://doi.org/10.23638/LMCS-15(4:15)2019 https://doi.org/10.23638/LMCS-15(4:15)2019 Leroux, J. Praveen, M. Schnoebelen, Ph. Sutre, G. Leroux, J. Praveen, M. Schnoebelen, Ph. Sutre, G. 0 Definable isomorphism problem Wed, 11 Dec 2019 08:15:57 +0000 https://doi.org/10.23638/LMCS-15(4:14)2019 https://doi.org/10.23638/LMCS-15(4:14)2019 Keshvardoost, Khadijeh Klin, Bartek Lasota, Sławomir Ochremiak, Joanna Toruńczyk, Szymon Keshvardoost, Khadijeh Klin, Bartek Lasota, Sławomir Ochremiak, Joanna Toruńczyk, Szymon 0 A Curry-Howard Approach to Church's Synthesis Mon, 09 Dec 2019 09:38:16 +0000 https://doi.org/10.23638/LMCS-15(4:13)2019 https://doi.org/10.23638/LMCS-15(4:13)2019 Pradic, Pierre Riba, Colin Pradic, Pierre Riba, Colin 0 Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity Wed, 04 Dec 2019 08:48:13 +0000 https://doi.org/10.23638/LMCS-15(4:12)2019 https://doi.org/10.23638/LMCS-15(4:12)2019 Knop, Dušan Koutecký, Martin Masařík, Tomáš Toufar, Tomáš Knop, Dušan Koutecký, Martin Masařík, Tomáš Toufar, Tomáš 0 Computing the Width of Non-deterministic Automata Fri, 29 Nov 2019 19:57:45 +0000 https://doi.org/10.23638/LMCS-15(4:10)2019 https://doi.org/10.23638/LMCS-15(4:10)2019 Kuperberg, Denis Majumdar, Anirban Kuperberg, Denis Majumdar, Anirban 0 A non-regular language of infinite trees that is recognizable by a sort-wise finite algebra Fri, 29 Nov 2019 19:51:48 +0000 https://doi.org/10.23638/LMCS-15(4:11)2019 https://doi.org/10.23638/LMCS-15(4:11)2019 Bojańczyk, Mikołaj Klin, Bartek Bojańczyk, Mikołaj Klin, Bartek 0 Flow Logic \gamma$ or $\geq \gamma$, for $\gamma \in \mathbb{N}$, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to ${\rm P}^{\rm NP}$, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time. Finally, we introduce and study the query-checking problem for BFL*, where under-specified BFL* formulas are used for network exploration.]]> Thu, 14 Nov 2019 09:04:56 +0000 https://doi.org/10.23638/LMCS-15(4:9)2019 https://doi.org/10.23638/LMCS-15(4:9)2019 Kupferman, Orna Vardi, Gal Kupferman, Orna Vardi, Gal \gamma$ or $\geq \gamma$, for $\gamma \in \mathbb{N}$, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to ${\rm P}^{\rm NP}$, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time. Finally, we introduce and study the query-checking problem for BFL*, where under-specified BFL* formulas are used for network exploration.]]> 0 Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories Thu, 07 Nov 2019 08:04:24 +0000 https://doi.org/10.23638/LMCS-15(4:8)2019 https://doi.org/10.23638/LMCS-15(4:8)2019 Lemay, Jean-Simon Pacaud Lemay, Jean-Simon Pacaud 0 The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter Wed, 30 Oct 2019 14:09:59 +0000 https://doi.org/10.23638/LMCS-15(4:7)2019 https://doi.org/10.23638/LMCS-15(4:7)2019 Muroya, Koko Ghica, Dan R. Muroya, Koko Ghica, Dan R. 0 On completeness and parametricity in the realizability semantics of System F Tue, 29 Oct 2019 13:05:39 +0000 https://doi.org/10.23638/LMCS-15(4:6)2019 https://doi.org/10.23638/LMCS-15(4:6)2019 Pistone, Paolo Pistone, Paolo 0 Scalar and Vectorial mu-calculus with Atoms Tue, 29 Oct 2019 12:56:46 +0000 https://doi.org/10.23638/LMCS-15(4:5)2019 https://doi.org/10.23638/LMCS-15(4:5)2019 Klin, Bartek Łełyk, Mateusz Klin, Bartek Łełyk, Mateusz 0 On Free $\omega$-Continuous and Regular Ordered Algebras Tue, 29 Oct 2019 07:55:27 +0000 https://doi.org/10.23638/LMCS-15(4:4)2019 https://doi.org/10.23638/LMCS-15(4:4)2019 Esik, Zoltan Kozen, Dexter Esik, Zoltan Kozen, Dexter 0 On the enumeration of closures and environments with an application to random generation Thu, 17 Oct 2019 11:53:48 +0000 https://doi.org/10.23638/LMCS-15(4:3)2019 https://doi.org/10.23638/LMCS-15(4:3)2019 Bendkowski, Maciej Lescanne, Pierre Bendkowski, Maciej Lescanne, Pierre 0 $\aleph_1$ and the modal $\mu$-calculus Tue, 15 Oct 2019 12:00:04 +0000 https://doi.org/10.23638/LMCS-15(4:1)2019 https://doi.org/10.23638/LMCS-15(4:1)2019 Gouveia, Maria João Santocanale, Luigi Gouveia, Maria João Santocanale, Luigi 0 Rule Formats for Nominal Process Calculi Mon, 14 Oct 2019 08:04:06 +0000 https://doi.org/10.23638/LMCS-15(4:2)2019 https://doi.org/10.23638/LMCS-15(4:2)2019 Aceto, Luca Fábregas, Ignacio García-Pérez, Álvaro Ingólfsdóttir, Anna Ortega-Mallén, Yolanda Aceto, Luca Fábregas, Ignacio García-Pérez, Álvaro Ingólfsdóttir, Anna Ortega-Mallén, Yolanda 0 The Complexity of Flat Freeze LTL Mon, 30 Sep 2019 08:07:08 +0000 https://doi.org/10.23638/LMCS-15(3:33)2019 https://doi.org/10.23638/LMCS-15(3:33)2019 Bollig, Benedikt Quaas, Karin Sangnier, Arnaud Bollig, Benedikt Quaas, Karin Sangnier, Arnaud 0 The parameterized space complexity of model-checking bounded variable first-order logic Fri, 20 Sep 2019 09:48:31 +0000 https://doi.org/10.23638/LMCS-15(3:31)2019 https://doi.org/10.23638/LMCS-15(3:31)2019 Chen, Yijia Elberfeld, Michael Müller, Moritz Chen, Yijia Elberfeld, Michael Müller, Moritz 0 Nash Equilibrium and Bisimulation Invariance Fri, 20 Sep 2019 09:46:29 +0000 https://doi.org/10.23638/LMCS-15(3:32)2019 https://doi.org/10.23638/LMCS-15(3:32)2019 Gutierrez, Julian Harrenstein, Paul Perelli, Giuseppe Wooldridge, Michael Gutierrez, Julian Harrenstein, Paul Perelli, Giuseppe Wooldridge, Michael 0 On noncommutative extensions of linear logic Fri, 20 Sep 2019 08:05:41 +0000 https://doi.org/10.23638/LMCS-15(3:30)2019 https://doi.org/10.23638/LMCS-15(3:30)2019 Slavnov, Sergey Slavnov, Sergey 0 Definability and Interpolation within Decidable Fixpoint Logics Tue, 10 Sep 2019 08:00:35 +0000 https://doi.org/10.23638/LMCS-15(3:29)2019 https://doi.org/10.23638/LMCS-15(3:29)2019 Benedikt, Michael Bourhis, Pierre Boom, Michael Vanden Benedikt, Michael Bourhis, Pierre Boom, Michael Vanden 0 Higher-dimensional automata modeling shared-variable systems Fri, 06 Sep 2019 13:19:57 +0000 https://doi.org/10.23638/LMCS-15(3:28)2019 https://doi.org/10.23638/LMCS-15(3:28)2019 Kahl, Thomas Kahl, Thomas 0 Regular tree languages in low levels of the Wadge Hierarchy Wed, 04 Sep 2019 11:27:55 +0000 https://doi.org/10.23638/LMCS-15(3:27)2019 https://doi.org/10.23638/LMCS-15(3:27)2019 Bojańczyk, Mikołaj Cavallari, Filippo Place, Thomas Skrzypczak, Michał Bojańczyk, Mikołaj Cavallari, Filippo Place, Thomas Skrzypczak, Michał 0 A diagrammatic calculus of fermionic quantum circuits Mon, 02 Sep 2019 09:29:03 +0000 https://doi.org/10.23638/LMCS-15(3:26)2019 https://doi.org/10.23638/LMCS-15(3:26)2019 de Felice, Giovanni Hadzihasanovic, Amar Ng, Kang Feng de Felice, Giovanni Hadzihasanovic, Amar Ng, Kang Feng 0 Interaction Graphs: Exponentials Fri, 30 Aug 2019 09:42:44 +0000 https://doi.org/10.23638/LMCS-15(3:25)2019 https://doi.org/10.23638/LMCS-15(3:25)2019 Seiller, Thomas Seiller, Thomas 0 Approximability in the GPAC Thu, 29 Aug 2019 10:59:26 +0000 https://doi.org/10.23638/LMCS-15(3:24)2019 https://doi.org/10.23638/LMCS-15(3:24)2019 Poças, Diogo Zucker, Jeffery Poças, Diogo Zucker, Jeffery 0 The Data Complexity of Ontology-Mediated Queries with Closed Predicates Wed, 28 Aug 2019 10:41:02 +0000 https://doi.org/10.23638/LMCS-15(3:23)2019 https://doi.org/10.23638/LMCS-15(3:23)2019 Lutz, Carsten Seylan, Inanc Wolter, Frank Lutz, Carsten Seylan, Inanc Wolter, Frank 0 Alternating, private alternating, and quantum alternating realtime automata Wed, 28 Aug 2019 10:38:14 +0000 https://doi.org/10.23638/LMCS-15(3:22)2019 https://doi.org/10.23638/LMCS-15(3:22)2019 Demirci, Gökalp Hirvensalo, Mika Reinhardt, Klaus Say, A. C. Cem Yakaryılmaz, Abuzer Demirci, Gökalp Hirvensalo, Mika Reinhardt, Klaus Say, A. C. Cem Yakaryılmaz, Abuzer 0 Query learning of derived $\omega$-tree languages in polynomial time Tue, 27 Aug 2019 06:58:33 +0000 https://doi.org/10.23638/LMCS-15(3:21)2019 https://doi.org/10.23638/LMCS-15(3:21)2019 Angluin, Dana Antonopoulos, Timos Fisman, Dana Angluin, Dana Antonopoulos, Timos Fisman, Dana 0 Parity Games with Weights Fri, 23 Aug 2019 08:27:26 +0000 https://doi.org/10.23638/LMCS-15(3:20)2019 https://doi.org/10.23638/LMCS-15(3:20)2019 Schewe, Sven Weinert, Alexander Zimmermann, Martin Schewe, Sven Weinert, Alexander Zimmermann, Martin 0 Abstract Completion, Formalized Wed, 21 Aug 2019 07:58:47 +0000 https://doi.org/10.23638/LMCS-15(3:19)2019 https://doi.org/10.23638/LMCS-15(3:19)2019 Hirokawa, Nao Middeldorp, Aart Sternagel, Christian Winkler, Sarah Hirokawa, Nao Middeldorp, Aart Sternagel, Christian Winkler, Sarah 0 Bounded Quantifier Instantiation for Checking Inductive Invariants Wed, 21 Aug 2019 07:55:49 +0000 https://doi.org/10.23638/LMCS-15(3:18)2019 https://doi.org/10.23638/LMCS-15(3:18)2019 Feldman, Yotam M. Y. Padon, Oded Immerman, Neil Sagiv, Mooly Shoham, Sharon Feldman, Yotam M. Y. Padon, Oded Immerman, Neil Sagiv, Mooly Shoham, Sharon 0 On the Succinctness of Atoms of Dependency Tue, 20 Aug 2019 08:30:03 +0000 https://doi.org/10.23638/LMCS-15(3:17)2019 https://doi.org/10.23638/LMCS-15(3:17)2019 Lück, Martin Vilander, Miikka Lück, Martin Vilander, Miikka 0 Quantitative Automata under Probabilistic Semantics Tue, 13 Aug 2019 10:06:56 +0000 https://doi.org/10.23638/LMCS-15(3:16)2019 https://doi.org/10.23638/LMCS-15(3:16)2019 Chatterjee, Krishnendu Henzinger, Thomas A. Otop, Jan Chatterjee, Krishnendu Henzinger, Thomas A. Otop, Jan 0 A categorical semantics for causal structure Fri, 09 Aug 2019 09:48:56 +0000 https://doi.org/10.23638/LMCS-15(3:15)2019 https://doi.org/10.23638/LMCS-15(3:15)2019 Kissinger, Aleks Uijlen, Sander Kissinger, Aleks Uijlen, Sander 0 Companions, Causality and Codensity Thu, 08 Aug 2019 08:19:22 +0000 https://doi.org/10.23638/LMCS-15(3:14)2019 https://doi.org/10.23638/LMCS-15(3:14)2019 Pous, Damien Rot, Jurriaan Pous, Damien Rot, Jurriaan 0 On the commutativity of the powerspace constructions Thu, 08 Aug 2019 08:16:28 +0000 https://doi.org/10.23638/LMCS-15(3:13)2019 https://doi.org/10.23638/LMCS-15(3:13)2019 de Brecht, Matthew Kawai, Tatsuji de Brecht, Matthew Kawai, Tatsuji 0 Divergence and unique solution of equations Wed, 07 Aug 2019 09:05:42 +0000 https://doi.org/10.23638/LMCS-15(3:12)2019 https://doi.org/10.23638/LMCS-15(3:12)2019 Durier, Adrien Hirschkoff, Daniel Sangiorgi, Davide Durier, Adrien Hirschkoff, Daniel Sangiorgi, Davide 0 Game characterizations and lower cones in the Weihrauch degrees Tue, 06 Aug 2019 12:55:12 +0000 https://doi.org/10.23638/LMCS-15(3:11)2019 https://doi.org/10.23638/LMCS-15(3:11)2019 Nobrega, Hugo Pauly, Arno Nobrega, Hugo Pauly, Arno 0 Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs Thu, 01 Aug 2019 12:53:50 +0000 https://doi.org/10.23638/LMCS-15(3:10)2019 https://doi.org/10.23638/LMCS-15(3:10)2019 Berardi, Stefano Tatsuta, Makoto Berardi, Stefano Tatsuta, Makoto 0 Normalizing the Taylor expansion of non-deterministic {\lambda}-terms, via parallel reduction of resource vectors Wed, 31 Jul 2019 10:58:47 +0000 https://doi.org/10.23638/LMCS-15(3:9)2019 https://doi.org/10.23638/LMCS-15(3:9)2019 Vaux, Lionel Vaux, Lionel 0 An efficient algorithm to decide periodicity of $b$-recognisable sets using LSDF convention Wed, 31 Jul 2019 09:23:14 +0000 https://doi.org/10.23638/LMCS-15(3:8)2019 https://doi.org/10.23638/LMCS-15(3:8)2019 Marsault, Victor Marsault, Victor 0 Controlling a population Mon, 29 Jul 2019 11:57:05 +0000 https://doi.org/10.23638/LMCS-15(3:6)2019 https://doi.org/10.23638/LMCS-15(3:6)2019 Bertrand, Nathalie Dewaskar, Miheer Genest, Blaise Gimbert, Hugo Godbole, Adwait Amit Bertrand, Nathalie Dewaskar, Miheer Genest, Blaise Gimbert, Hugo Godbole, Adwait Amit 0 A Forgotten Theory of Proofs ? Mon, 29 Jul 2019 11:53:20 +0000 https://doi.org/10.23638/LMCS-15(3:7)2019 https://doi.org/10.23638/LMCS-15(3:7)2019 Engeler, Erwin Engeler, Erwin 0 Coherence for Frobenius pseudomonoids and the geometry of linear proofs Fri, 26 Jul 2019 07:12:17 +0000 https://doi.org/10.23638/LMCS-15(3:5)2019 https://doi.org/10.23638/LMCS-15(3:5)2019 Dunn, Lawrence Vicary, Jamie Dunn, Lawrence Vicary, Jamie 0 Logical properties of random graphs from small addable classes Thu, 25 Jul 2019 12:06:17 +0000 https://doi.org/10.23638/LMCS-15(3:4)2019 https://doi.org/10.23638/LMCS-15(3:4)2019 Dawar, Anuj Kopczyński, Eryk Dawar, Anuj Kopczyński, Eryk 0 Subspace-Invariant AC$^0$ Formulas Wed, 24 Jul 2019 08:45:16 +0000 https://doi.org/10.23638/LMCS-15(3:3)2019 https://doi.org/10.23638/LMCS-15(3:3)2019 Rossman, Benjamin Rossman, Benjamin 0 Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs Mon, 08 Jul 2019 08:51:28 +0000 https://doi.org/10.23638/LMCS-15(3:2)2019 https://doi.org/10.23638/LMCS-15(3:2)2019 Grußien, Berit Grußien, Berit 0 Guarded and Unguarded Iteration for Generalized Processes Thu, 04 Jul 2019 07:53:01 +0000 https://doi.org/10.23638/LMCS-15(3:1)2019 https://doi.org/10.23638/LMCS-15(3:1)2019 Goncharov, Sergey Schröder, Lutz Rauch, Christoph Piróg, Maciej Goncharov, Sergey Schröder, Lutz Rauch, Christoph Piróg, Maciej 0 Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies Tue, 25 Jun 2019 14:50:24 +0000 https://doi.org/10.23638/LMCS-15(2:21)2019 https://doi.org/10.23638/LMCS-15(2:21)2019 Maietti, Maria Emilia Pasquali, Fabio Rosolini, Giuseppe Maietti, Maria Emilia Pasquali, Fabio Rosolini, Giuseppe 0 Regular Separability of One Counter Automata Tue, 11 Jun 2019 08:07:00 +0000 https://doi.org/10.23638/LMCS-15(2:20)2019 https://doi.org/10.23638/LMCS-15(2:20)2019 Czerwiński, Wojciech Lasota, Sławomir Czerwiński, Wojciech Lasota, Sławomir 0 Upper Bounds on the Quantifier Depth for Graph Differentiation in First-Order Logic Thu, 30 May 2019 11:30:17 +0000 https://doi.org/10.23638/LMCS-15(2:19)2019 https://doi.org/10.23638/LMCS-15(2:19)2019 Kiefer, Sandra Schweitzer, Pascal Kiefer, Sandra Schweitzer, Pascal 0 Bisimulations for Delimited-Control Operators Fri, 24 May 2019 08:10:10 +0000 https://doi.org/10.23638/LMCS-15(2:18)2019 https://doi.org/10.23638/LMCS-15(2:18)2019 Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr Biernacki, Dariusz Lenglet, Sergueï Polesiuk, Piotr 0 An $\omega$-Algebra for Real-Time Energy Problems Fri, 24 May 2019 08:06:49 +0000 https://doi.org/10.23638/LMCS-15(2:17)2019 https://doi.org/10.23638/LMCS-15(2:17)2019 Cachera, David Fahrenberg, Uli Legay, Axel Cachera, David Fahrenberg, Uli Legay, Axel 0 The logical strength of Büchi's decidability theorem Thu, 23 May 2019 08:51:13 +0000 https://doi.org/10.23638/LMCS-15(2:16)2019 https://doi.org/10.23638/LMCS-15(2:16)2019 Kołodziejczyk, Leszek Michalewski, Henryk Pradic, Pierre Skrzypczak, Michał Kołodziejczyk, Leszek Michalewski, Henryk Pradic, Pierre Skrzypczak, Michał 0 Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics Thu, 23 May 2019 08:37:19 +0000 https://doi.org/10.23638/LMCS-15(2:15)2019 https://doi.org/10.23638/LMCS-15(2:15)2019 Feier, Cristina Kuusisto, Antti Lutz, Carsten Feier, Cristina Kuusisto, Antti Lutz, Carsten 0 Every metric space is separable in function realizability Thu, 23 May 2019 08:34:32 +0000 https://doi.org/10.23638/LMCS-15(2:14)2019 https://doi.org/10.23638/LMCS-15(2:14)2019 Bauer, Andrej Swan, Andrew Bauer, Andrej Swan, Andrew 0 On the Expressiveness and Monitoring of Metric Temporal Logic Fri, 10 May 2019 07:54:27 +0000 https://doi.org/10.23638/LMCS-15(2:13)2019 https://doi.org/10.23638/LMCS-15(2:13)2019 Ho, Hsi-Ming Ouaknine, Joël Worrell, James Ho, Hsi-Ming Ouaknine, Joël Worrell, James 0 A Denotational Semantics for SPARC TSO Wed, 08 May 2019 08:02:32 +0000 https://doi.org/10.23638/LMCS-15(2:10)2019 https://doi.org/10.23638/LMCS-15(2:10)2019 Kavanagh, Ryan Brookes, Stephen Kavanagh, Ryan Brookes, Stephen 0 A Strategy for Dynamic Programs: Start over and Muddle through Wed, 08 May 2019 07:25:11 +0000 https://doi.org/10.23638/LMCS-15(2:12)2019 https://doi.org/10.23638/LMCS-15(2:12)2019 Datta, Samir Mukherjee, Anish Schwentick, Thomas Vortmeier, Nils Zeume, Thomas Datta, Samir Mukherjee, Anish Schwentick, Thomas Vortmeier, Nils Zeume, Thomas 0 Covering and separation for logical fragments with modular predicates Wed, 08 May 2019 07:21:42 +0000 https://doi.org/10.23638/LMCS-15(2:11)2019 https://doi.org/10.23638/LMCS-15(2:11)2019 Place, Thomas Ramanathan, Varun Weil, Pascal Place, Thomas Ramanathan, Varun Weil, Pascal 0 Polishness of some topologies related to word or tree automata Wed, 08 May 2019 07:18:39 +0000 https://doi.org/10.23638/LMCS-15(2:9)2019 https://doi.org/10.23638/LMCS-15(2:9)2019 Finkel, Olivier Carton, Olivier Lecomte, Dominique Finkel, Olivier Carton, Olivier Lecomte, Dominique 0 Reasoning about effects: from lists to cyber-physical agents Tue, 30 Apr 2019 07:29:54 +0000 https://doi.org/10.23638/LMCS-15(2:8)2019 https://doi.org/10.23638/LMCS-15(2:8)2019 Mason, Ian A. Talcott, Carolyn L. Mason, Ian A. Talcott, Carolyn L. 0 Feedback computability on Cantor space Tue, 30 Apr 2019 07:27:22 +0000 https://doi.org/10.23638/LMCS-15(2:7)2019 https://doi.org/10.23638/LMCS-15(2:7)2019 Ackerman, Nathanael L. Freer, Cameron E. Lubarsky, Robert S. Ackerman, Nathanael L. Freer, Cameron E. Lubarsky, Robert S. 0 The height of piecewise-testable languages and the complexity of the logic of subwords Tue, 30 Apr 2019 07:23:39 +0000 https://doi.org/10.23638/LMCS-15(2:6)2019 https://doi.org/10.23638/LMCS-15(2:6)2019 Karandikar, Prateek Schnoebelen, Philippe Karandikar, Prateek Schnoebelen, Philippe 0 All-Path Reachability Logic Tue, 30 Apr 2019 07:20:52 +0000 https://doi.org/10.23638/LMCS-15(2:5)2019 https://doi.org/10.23638/LMCS-15(2:5)2019 Stefanescu, Andrei Ciobaca, Stefan Mereuta, Radu Moore, Brandon Serbanuta, Traian Florin Rosu, Grigore Stefanescu, Andrei Ciobaca, Stefan Mereuta, Radu Moore, Brandon Serbanuta, Traian Florin Rosu, Grigore 0 Validity and Entailment in Modal and Propositional Dependence Logics Fri, 26 Apr 2019 11:19:52 +0000 https://doi.org/10.23638/LMCS-15(2:4)2019 https://doi.org/10.23638/LMCS-15(2:4)2019 Hannula, Miika Hannula, Miika 0 Generalised Mermin-type non-locality arguments Fri, 26 Apr 2019 11:15:46 +0000 https://doi.org/10.23638/LMCS-15(2:3)2019 https://doi.org/10.23638/LMCS-15(2:3)2019 Gogioso, Stefano Zeng, William Gogioso, Stefano Zeng, William 0 Canonical Models and the Complexity of Modal Team Logic Thu, 11 Apr 2019 07:56:04 +0000 https://doi.org/10.23638/LMCS-15(2:2)2019 https://doi.org/10.23638/LMCS-15(2:2)2019 Lück, Martin Lück, Martin 0 Streamability of nested word transductions Thu, 04 Apr 2019 09:07:29 +0000 https://doi.org/10.23638/LMCS-15(2:1)2019 https://doi.org/10.23638/LMCS-15(2:1)2019 Filiot, Emmanuel Gauwin, Olivier Reynier, Pierre-Alain Servais, Frédéric Filiot, Emmanuel Gauwin, Olivier Reynier, Pierre-Alain Servais, Frédéric 0 Abstract Hidden Markov Models: a monadic account of quantitative information flow Fri, 29 Mar 2019 20:53:26 +0000 https://doi.org/10.23638/LMCS-15(1:36)2019 https://doi.org/10.23638/LMCS-15(1:36)2019 McIver, Annabelle Morgan, Carroll Rabehaja, Tahiry McIver, Annabelle Morgan, Carroll Rabehaja, Tahiry 0 Moschovakis Extension of Represented Spaces Fri, 29 Mar 2019 20:34:53 +0000 https://doi.org/10.23638/LMCS-15(1:35)2019 https://doi.org/10.23638/LMCS-15(1:35)2019 Skordev, Dimiter Skordev, Dimiter 0 Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture Fri, 29 Mar 2019 20:30:28 +0000 https://doi.org/10.23638/LMCS-15(1:34)2019 https://doi.org/10.23638/LMCS-15(1:34)2019 Janičić, Predrag Marić, Filip Maliković, Marko Janičić, Predrag Marić, Filip Maliković, Marko 0 On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory Fri, 29 Mar 2019 20:11:08 +0000 https://doi.org/10.23638/LMCS-15(1:33)2019 https://doi.org/10.23638/LMCS-15(1:33)2019 Jeffrey, Alan Riely, James Jeffrey, Alan Riely, James 0 A classical groupoid model for quantum networks Fri, 29 Mar 2019 18:15:38 +0000 https://doi.org/10.23638/LMCS-15(1:32)2019 https://doi.org/10.23638/LMCS-15(1:32)2019 Reutter, David J. Vicary, Jamie Reutter, David J. Vicary, Jamie 0 Proving Soundness of Extensional Normal-Form Bisimilarities Fri, 29 Mar 2019 09:04:14 +0000 https://doi.org/10.23638/LMCS-15(1:31)2019 https://doi.org/10.23638/LMCS-15(1:31)2019 Biernacki, Dariusz Lenglet, Serguei Polesiuk, Piotr Biernacki, Dariusz Lenglet, Serguei Polesiuk, Piotr 0 Topological Scott Convergence Theorem Fri, 22 Mar 2019 08:27:26 +0000 https://doi.org/10.23638/LMCS-15(1:29)2019 https://doi.org/10.23638/LMCS-15(1:29)2019 Andradi, Hadrian Ho, Weng Kin Andradi, Hadrian Ho, Weng Kin 0 Initial Semantics for Reduction Rules Thu, 21 Mar 2019 07:22:53 +0000 https://doi.org/10.23638/LMCS-15(1:28)2019 https://doi.org/10.23638/LMCS-15(1:28)2019 Ahrens, Benedikt Ahrens, Benedikt 0 Stone-Type Dualities for Separation Logics Thu, 14 Mar 2019 09:54:00 +0000 https://doi.org/10.23638/LMCS-15(1:27)2019 https://doi.org/10.23638/LMCS-15(1:27)2019 Docherty, Simon Pym, David Docherty, Simon Pym, David 0 On the First-Order Complexity of Induced Subgraph Isomorphism (1/2-o(1))t$, where the function in the little-o notation approaches 0 as $t$ inreases. This bound holds true even for a related parameter $W^*[F]\le W[F]$, which is defined as the minimum $k$ such that $I(F)$ is definable in the infinitary logic $L^k_{\infty\omega}$. We show that $W^*[F]$ can be strictly less than $W[F]$. Specifically, $W^*[P_4]=3$ for $P_4$ being the path graph on 4 vertices. Using the lower bound for $W[F]$, we also obtain a succintness result for existential monadic second-order logic: A usage of just one monadic quantifier sometimes reduces the first-order quantifier depth at a super-recursive rate.]]> Wed, 06 Mar 2019 15:20:47 +0000 https://doi.org/10.23638/LMCS-15(1:25)2019 https://doi.org/10.23638/LMCS-15(1:25)2019 Verbitsky, Oleg Zhukovskii, Maksim Verbitsky, Oleg Zhukovskii, Maksim (1/2-o(1))t$, where the function in the little-o notation approaches 0 as $t$ inreases. This bound holds true even for a related parameter $W^*[F]\le W[F]$, which is defined as the minimum $k$ such that $I(F)$ is definable in the infinitary logic $L^k_{\infty\omega}$. We show that $W^*[F]$ can be strictly less than $W[F]$. Specifically, $W^*[P_4]=3$ for $P_4$ being the path graph on 4 vertices. Using the lower bound for $W[F]$, we also obtain a succintness result for existential monadic second-order logic: A usage of just one monadic quantifier sometimes reduces the first-order quantifier depth at a super-recursive rate.]]> 0 Capturing Polynomial Time using Modular Decomposition Tue, 05 Mar 2019 20:03:47 +0000 https://doi.org/10.23638/LMCS-15(1:24)2019 https://doi.org/10.23638/LMCS-15(1:24)2019 Grußien, Berit Grußien, Berit 0 Web spaces and worldwide web spaces: topological aspects of domain theory Tue, 05 Mar 2019 20:01:06 +0000 https://doi.org/10.23638/LMCS-15(1:23)2019 https://doi.org/10.23638/LMCS-15(1:23)2019 Erné, Marcel Erné, Marcel 0 The principle of pointfree continuity Tue, 05 Mar 2019 19:58:39 +0000 https://doi.org/10.23638/LMCS-15(1:22)2019 https://doi.org/10.23638/LMCS-15(1:22)2019 Kawai, Tatsuji Sambin, Giovanni Kawai, Tatsuji Sambin, Giovanni 0 On the Incomparability of Cache Algorithms in Terms of Timing Leakage Tue, 05 Mar 2019 19:56:59 +0000 https://doi.org/10.23638/LMCS-15(1:21)2019 https://doi.org/10.23638/LMCS-15(1:21)2019 Cañones, Pablo Köpf, Boris Reineke, Jan Cañones, Pablo Köpf, Boris Reineke, Jan 0 Displayed Categories C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.]]> Tue, 05 Mar 2019 19:55:20 +0000 https://doi.org/10.23638/LMCS-15(1:20)2019 https://doi.org/10.23638/LMCS-15(1:20)2019 Ahrens, Benedikt Lumsdaine, Peter LeFanu Ahrens, Benedikt Lumsdaine, Peter LeFanu C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.]]> 0 Shortest paths in one-counter systems Tue, 05 Mar 2019 19:51:35 +0000 https://doi.org/10.23638/LMCS-15(1:19)2019 https://doi.org/10.23638/LMCS-15(1:19)2019 Chistikov, Dmitry Czerwiński, Wojciech Hofman, Piotr Pilipczuk, Michał Wehar, Michael Chistikov, Dmitry Czerwiński, Wojciech Hofman, Piotr Pilipczuk, Michał Wehar, Michael 0 Thin Games with Symmetry and Concurrent Hyland-Ong Games Mon, 04 Mar 2019 11:35:36 +0000 https://doi.org/10.23638/LMCS-15(1:18)2019 https://doi.org/10.23638/LMCS-15(1:18)2019 Castellan, Simon Clairambault, Pierre Winskel, Glynn Castellan, Simon Clairambault, Pierre Winskel, Glynn 0 Behavioural equivalences for timed systems Thu, 28 Feb 2019 20:40:01 +0000 https://doi.org/10.23638/LMCS-15(1:17)2019 https://doi.org/10.23638/LMCS-15(1:17)2019 Brengos, Tomasz Peressotti, Marco Brengos, Tomasz Peressotti, Marco 0 Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence Fri, 22 Feb 2019 09:04:17 +0000 https://doi.org/10.23638/LMCS-15(1:16)2019 https://doi.org/10.23638/LMCS-15(1:16)2019 Asada, Kazuyuki Kobayashi, Naoki Sin'ya, Ryoma Tsukada, Takeshi Asada, Kazuyuki Kobayashi, Naoki Sin'ya, Ryoma Tsukada, Takeshi 0 Sahlqvist via Translation Fri, 22 Feb 2019 08:55:28 +0000 https://doi.org/10.23638/LMCS-15(1:15)2019 https://doi.org/10.23638/LMCS-15(1:15)2019 Conradie, Willem Palmigiano, Alessandra Zhao, Zhiguang Conradie, Willem Palmigiano, Alessandra Zhao, Zhiguang 0 Algebra, coalgebra, and minimization in polynomial differential equations Fri, 15 Feb 2019 10:21:29 +0000 https://doi.org/10.23638/LMCS-15(1:14)2019 https://doi.org/10.23638/LMCS-15(1:14)2019 Boreale, Michele Boreale, Michele 0 Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs Wed, 13 Feb 2019 10:01:53 +0000 https://doi.org/10.23638/LMCS-15(1:13)2019 https://doi.org/10.23638/LMCS-15(1:13)2019 Beyersdorff, Olaf Blinkhorn, Joshua Hinde, Luke Beyersdorff, Olaf Blinkhorn, Joshua Hinde, Luke 0 The Subpower Membership Problem for Finite Algebras with Cube Terms Wed, 13 Feb 2019 07:32:20 +0000 https://doi.org/10.23638/LMCS-15(1:11)2019 https://doi.org/10.23638/LMCS-15(1:11)2019 Bulatov, Andrei Mayr, Peter Szendrei, Ágnes Bulatov, Andrei Mayr, Peter Szendrei, Ágnes 0 Efficient reduction of nondeterministic automata with application to language inclusion testing Tue, 12 Feb 2019 23:00:00 +0000 https://doi.org/10.23638/LMCS-15(1:12)2019 https://doi.org/10.23638/LMCS-15(1:12)2019 Clemente, Lorenzo Mayr, Richard Clemente, Lorenzo Mayr, Richard 0 Relative Entailment Among Probabilistic Implications Wed, 06 Feb 2019 11:01:26 +0000 https://doi.org/10.23638/LMCS-15(1:10)2019 https://doi.org/10.23638/LMCS-15(1:10)2019 Atserias, Albert Balcázar, José L. Piceno, Marie Ely Atserias, Albert Balcázar, José L. Piceno, Marie Ely 0 A sequent calculus for a semi-associative law Tue, 05 Feb 2019 09:24:57 +0000 https://doi.org/10.23638/LMCS-15(1:9)2019 https://doi.org/10.23638/LMCS-15(1:9)2019 Zeilberger, Noam Zeilberger, Noam 0 A Light Modality for Recursion Tue, 05 Feb 2019 09:15:45 +0000 https://doi.org/10.23638/LMCS-15(1:8)2019 https://doi.org/10.23638/LMCS-15(1:8)2019 Severi, Paula Severi, Paula 0 Shrub-depth: Capturing Height of Dense Graphs Thu, 31 Jan 2019 10:18:55 +0000 https://doi.org/10.23638/LMCS-15(1:7)2019 https://doi.org/10.23638/LMCS-15(1:7)2019 Ganian, Robert Hliněný, Petr Nešetřil, Jaroslav Obdržálek, Jan de Mendez, Patrice Ossona Ganian, Robert Hliněný, Petr Nešetřil, Jaroslav Obdržálek, Jan de Mendez, Patrice Ossona 0 Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture Tue, 29 Jan 2019 13:56:50 +0000 https://doi.org/10.23638/LMCS-15(1:6)2019 htt