Logic in Computer Science

Authors and titles for cs.LO in May 2021

[1]  arXiv:2105.00024 [pdf, other]

Title: Types are Internal $\infty$-Groupoids

Authors: Antoine Allioux, Eric Finster, Matthieu Sozeau

Comments: Extended version of the LICS 2021 article

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[2]  arXiv:2105.00188 [pdf, ps, other]

Title: lr-Multisemigroups and Modal Convolution Algebras

Authors: Uli Fahrenberg, Christian Johnsen, Georg Struth, Krzysztof Ziemiański

Comments: 38 pages, 1 figure

Subjects: Logic in Computer Science (cs.LO); Rings and Algebras (math.RA)

[3]  arXiv:2105.00564 [pdf, other]

Title: Encoding Tight Typing in a Unified Framework

Authors: Delia Kesner, Andrés Viso

Comments: arXiv admin note: text overlap with arXiv:2002.04011

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[4]  arXiv:2105.00669 [pdf, other]

Title: Explaining Behavioural Inequivalence Generically in Quasilinear Time

Authors: Thorsten Wißmann, Stefan Milius, Lutz Schröder

Comments: Full version with appendix containing all proofs

Subjects: Logic in Computer Science (cs.LO)

[5]  arXiv:2105.00735 [pdf, ps, other]

Title: In search of lost time: Axiomatising parallel composition in process algebras

Authors: Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingolfsdottir, Bas Luttik

Comments: arXiv admin note: text overlap with arXiv:2010.01943, arXiv:2102.11166

Subjects: Logic in Computer Science (cs.LO)

[6]  arXiv:2105.00748 [pdf, ps, other]

Title: What's Decidable about (Atomic) Polymorphism

Authors: Paolo Pistone, Luca Tranchini

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[7]  arXiv:2105.00885 [pdf, ps, other]

Title: Generating Extended Resolution Proofs with a BDD-Based SAT Solver

Authors: Randal E. Bryant, Marijn J. H. Heule

Comments: Extended version of paper published at TACAS 2021

Subjects: Logic in Computer Science (cs.LO)

[8]  arXiv:2105.00969 [pdf, other]

Title: Abstract clones for abstract syntax

Authors: Nathanael Arkor, Dylan McDermott

Comments: To appear in the proceedings of FSCD 2021; 16 pages

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[9]  arXiv:2105.01382 [pdf, other]

Title: A Subatomic Proof System for Decision Trees

Authors: Chris Barrett, Alessio Guglielmi

Comments: To appear on ACM Transactions on Computational Logic

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[10]  arXiv:2105.01861 [pdf, other]

Title: Higher-Order Model Checking Step by Step

Authors: Paweł Parys

Comments: This is an extended version of a paper published on the ICALP 2021 conference

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[11]  arXiv:2105.02013 [pdf, other]

Title: Flavours of Sequential Information Flow

Authors: Ezio Bartocci, Thomas Ferrère, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa

Subjects: Logic in Computer Science (cs.LO)

[12]  arXiv:2105.02309 [pdf, other]

Title: A Generalized Concurrent Rule Construction for Double-Pushout Rewriting

Authors: Jens Kosiol, Gabriele Taentzer

Comments: 36 pages, 33 figures, accepted for publication at the 14th International Conference on Graph Transformation (ICGT) 2021

Subjects: Logic in Computer Science (cs.LO)

[13]  arXiv:2105.02352 [src]

Title: Uniqueness typing for intersection types

Authors: Richard Statman, Andrew Polonsky

Comments: Superseded by arXiv:1809.08169v2

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[14]  arXiv:2105.02444 [pdf, ps, other]

Title: Parallelized sequential composition, pipelines, and hardware weak memory models

Authors: Robert J. Colvin

Subjects: Logic in Computer Science (cs.LO)

[15]  arXiv:2105.02485 [pdf, other]

Title: Positional Injectivity for Innocent Strategies

Authors: Lison Blondeau-Patissier (ENS Lyon), Pierre Clairambault (LIP, PLUME)

Journal-ref: 6TH INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION, Jul 2021, Buenos Aires, Argentina

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[16]  arXiv:2105.02559 [pdf, ps, other]

Title: Probablistic Bigraphs

Authors: Blair Archibald, Muffy Calder, Michele Sevegnani

Comments: 20 pages, 15 figures

Subjects: Logic in Computer Science (cs.LO)

[17]  arXiv:2105.02842 [pdf, other]

Title: Concurrency Theorems for Non-linear Rewriting Theories

Authors: Nicolas Behr (Université de Paris, CNRS, IRIF), Russ Harmer (Univ. Lyon, EnsL, UCBL, CNRS, LIP, France), Jean Krivine (Université de Paris, CNRS, IRIF)

Comments: 19+14 pages, LNCS style; ICGT 2021 conference paper extended version

Subjects: Logic in Computer Science (cs.LO)

[18]  arXiv:2105.03005 [pdf, ps, other]

Title: A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

Authors: Maximiliano Cristiá, Gianfranco Rossi

Comments: arXiv admin note: text overlap with arXiv:2102.05422

Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)

[19]  arXiv:2105.03274 [pdf, other]

Title: Lovász-Type Theorems and Game Comonads

Authors: Anuj Dawar, Tomáš Jakl, Luca Reggio

Comments: 23 pages. To appear in the Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT); Logic (math.LO)

[20]  arXiv:2105.03389 [pdf, ps, other]

Title: GADTs, Functoriality, Parametricity: Pick Two

Authors: Patricia Johann (Appalachian State University), Enrico Ghiorzi (Appalachian State University), Daniel Jeffries (Appalachian State University)

Comments: In Proceedings LSFA 2021, arXiv:2204.03415

Journal-ref: EPTCS 357, 2022, pp. 77-92

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[21]  arXiv:2105.04057 [pdf, other]

Title: Fast Automated Reasoning over String Diagrams using Multiway Causal Structure

Authors: Jonathan Gorard, Manojna Namuduri, Xerxes D. Arsiwalla

Comments: Submitted to Applied Category Theory 2021. 14 pages, 9 figures

Subjects: Logic in Computer Science (cs.LO); Discrete Mathematics (cs.DM)

[22]  arXiv:2105.04110 [pdf, ps, other]

Title: A Framework for Reasoning About LF Specifications

Authors: Mary Southern

Subjects: Logic in Computer Science (cs.LO)

[23]  arXiv:2105.04176 [pdf, other]

Title: HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Subjects: Logic in Computer Science (cs.LO)

[24]  arXiv:2105.04501 [pdf, other]

Title: Incorrectness Logic for Graph Programs

Authors: Christopher M. Poskitt

Comments: Accepted by the 14th International Conference on Graph Transformation (ICGT 2021)

Journal-ref: Proc. ICGT 2021, volume 12741 of LNCS, pages 81-101. Springer, 2021

Subjects: Logic in Computer Science (cs.LO)

[25]  arXiv:2105.04817 [pdf, other]

Title: Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Authors: Mayuko Kori, Ichiro Hasuo, Shin-ya Katsumata

Comments: 38 pages

Subjects: Logic in Computer Science (cs.LO); Computation and Language (cs.CL)

[26]  arXiv:2105.04929 [pdf, other]

Title: Asynchronous Template Games and the Gray Tensor Product of 2-Categories

Authors: Melliès Paul-André

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[27]  arXiv:2105.05133 [pdf, other]

Title: Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL

Authors: Simon Foster, Chung-Kil Hur, Jim Woodcock

Comments: 14 pages, submitted to CONCUR 2021

Subjects: Logic in Computer Science (cs.LO)

[28]  arXiv:2105.05763 [pdf, other]

Title: Iltis: Learning Logic in the Web

Authors: Gaetano Geck, Christine Quenkert, Marko Schmellenkamp, Jonas Schmidt, Felix Tschirbs, Fabian Vehlken, Thomas Zeume

Subjects: Logic in Computer Science (cs.LO)

[29]  arXiv:2105.06009 [pdf, other]

Title: Verification of the Incremental Merkle Tree Algorithm with Dafny

Authors: Franck Cassez

Comments: 16 pages

Subjects: Logic in Computer Science (cs.LO)

[30]  arXiv:2105.06186 [pdf, other]

Title: Tracelet Hopf Algebras and Decomposition Spaces (Extended Abstract)

Authors: Nicolas Behr (Université Paris Cité, IRIF, CNRS), Joachim Kock (Universitat Autònoma de Barcelona & Centre de Recerca Matemàtica)

Comments: In Proceedings ACT 2021, arXiv:2211.01102

Journal-ref: EPTCS 372, 2022, pp. 323-337

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[31]  arXiv:2105.06194 [pdf, other]

Title: Geometric Model Checking of Continuous Space

Authors: Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 4 (November 22, 2022) lmcs:9060

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computer Vision and Pattern Recognition (cs.CV); Graphics (cs.GR)

[32]  arXiv:2105.06202 [pdf, ps, other]

Title: Deciding FO-definability of regular languages

Authors: Agi Kurucz, Vladislav Ryzhikov, Yury Savateev, Michael Zakharyaschev

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[33]  arXiv:2105.06244 [pdf, other]

Title: A Graphical Calculus for Lagrangian Relations

Authors: Cole Comfort (University of Oxford), Aleks Kissinger (University of Oxford)

Comments: In Proceedings ACT 2021, arXiv:2211.01102

Journal-ref: EPTCS 372, 2022, pp. 338-351

Subjects: Logic in Computer Science (cs.LO); Mathematical Physics (math-ph); Category Theory (math.CT); Quantum Physics (quant-ph)

[34]  arXiv:2105.06575 [pdf, other]

Title: Merit and Blame Assignment with Kind 2

Authors: Daniel Larraz, Mickaël Laurent, Cesare Tinelli

Subjects: Logic in Computer Science (cs.LO)

[35]  arXiv:2105.06690 [pdf, other]

Title: On Bisimilarities for Closure Spaces - Preliminary Version

Authors: Vincenzo Ciancia, Diego Latella, Mieke Massink Erik de Vink

Subjects: Logic in Computer Science (cs.LO)

[36]  arXiv:2105.06723 [pdf, other]

Title: Bounded Reachability Problems are Decidable in FIFO Machines

Authors: Benedikt Bollig, Alain Finkel, Amrita Suresh

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 20, 2022) lmcs:7485

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[37]  arXiv:2105.06744 [pdf, other]

Title: A Separator Theorem for Hypergraphs and a CSP-SAT Algorithm

Authors: Michal Koucký, Vojtěch Rödl, Navid Talebanfard

Journal-ref: Logical Methods in Computer Science, Volume 17, Issue 4 (December 13, 2021) lmcs:7484

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[38]  arXiv:2105.06787 [pdf, ps, other]

Title: Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition

Authors: Robin Hirsch, Jaš Šemrl

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[39]  arXiv:2105.06908 [pdf, ps, other]

Title: From Multisets over Distributions to Distributions over Multisets

Authors: Bart Jacobs

Subjects: Logic in Computer Science (cs.LO)

[40]  arXiv:2105.07531 [pdf, ps, other]

Title: First-Order Reasoning and Efficient Semi-Algebraic Proofs

Authors: Fedor Part, Neil Thapen, Iddo Tzameret

Comments: A preliminary version of this work appears in 36th Ann. Symp. Logic Comput. Science (LICS) 2021

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[41]  arXiv:2105.07595 [pdf, ps, other]

Title: A Complete Axiomatisation for Divergence Preserving Branching Congruence of Finite-State Behaviours

Authors: Xinxin Liu, Tingting Yu

Comments: 13 pages. To be published in LICS2021

Subjects: Logic in Computer Science (cs.LO)

[42]  arXiv:2105.07663 [pdf, other]

Title: Summing Up Smart Transitions

Authors: Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv

Comments: This submission is an extended version of the CAV 2021 paper "Summing Up Smart Transitions", by N. Elad, S. Rain, N. Immerman, L. Kov\'acs and M. Sagiv

Subjects: Logic in Computer Science (cs.LO)

[43]  arXiv:2105.08155 [pdf, ps, other]

Title: (Deep) Induction Rules for GADTs

Authors: Patricia Johann, Enrico Ghiorzi

Comments: 14 pages

Subjects: Logic in Computer Science (cs.LO)

[44]  arXiv:2105.08231 [pdf, ps, other]

Title: The Topological Mu-Calculus: completeness and decidability

Authors: Alexandru Baltag, Nick Bezhanishvili, David Fernández-Duque

Subjects: Logic in Computer Science (cs.LO)

[45]  arXiv:2105.08353 [pdf, ps, other]

Title: Quantitative and Approximate Monitoring

Authors: Thomas A. Henzinger, N. Ege Saraç

Comments: To appear in LICS 2021; corrected a reference

Subjects: Logic in Computer Science (cs.LO)

[46]  arXiv:2105.08473 [pdf, other]

Title: An Internal Language for Categories Enriched over Generalised Metric Spaces

Authors: Fredrik Dahlqvist, Renato Neves

Comments: Extended version of the CSL'22 paper "An Internal Language for Categories Enriched over Generalised Metric Spaces"

Subjects: Logic in Computer Science (cs.LO)

[47]  arXiv:2105.08708 [pdf, other]

Title: A Spatial Logic for Simplicial Models

Authors: Michele Loreti, Michela Quadrini

Journal-ref: Logical Methods in Computer Science, Volume 19, Issue 3 (July 26, 2023) lmcs:8576

Subjects: Logic in Computer Science (cs.LO)

[48]  arXiv:2105.08951 [pdf, ps, other]

Title: On the logical structure of choice and bar induction principles

Authors: Nuria Brede, Hugo Herbelin (PI.R2)

Comments: LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy

Subjects: Logic in Computer Science (cs.LO)

[49]  arXiv:2105.09169 [pdf, other]

Title: Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR

Authors: Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker

Subjects: Logic in Computer Science (cs.LO)

[50]  arXiv:2105.09368 [pdf, ps, other]

Title: An Algebraic Characterisation of First-Order Logic with Neighbour

Authors: Amaldev Manuel, Dhruv Nevatia

Comments: 13 pages

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)