LIPIcs, Volume 171
CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)
Editors: Igor Konnov and Laura Kovács
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Martin Vassor and Nobuko Yoshida. Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 41:1-41:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vassor_et_al:LIPIcs.ECOOP.2024.41, author = {Vassor, Martin and Yoshida, Nobuko}, title = {{Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {41:1--41:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.41}, URN = {urn:nbn:de:0030-drops-208906}, doi = {10.4230/LIPIcs.ECOOP.2024.41}, annote = {Keywords: Message-Passing Concurrency, Session Types, Specification} }
Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)
Zekai Li, Amin Farjudian, and Heshan Du. A Logic of East and West for Intervals (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 17:1-17:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{li_et_al:LIPIcs.COSIT.2024.17, author = {Li, Zekai and Farjudian, Amin and Du, Heshan}, title = {{A Logic of East and West for Intervals}}, booktitle = {16th International Conference on Spatial Information Theory (COSIT 2024)}, pages = {17:1--17:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-330-0}, ISSN = {1868-8969}, year = {2024}, volume = {315}, editor = {Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.17}, URN = {urn:nbn:de:0030-drops-208320}, doi = {10.4230/LIPIcs.COSIT.2024.17}, annote = {Keywords: Qualitative Spatial Logic, Soundness, Completeness} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clune_et_al:LIPIcs.ITP.2024.10, author = {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy}, title = {{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {10:1--10:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10}, URN = {urn:nbn:de:0030-drops-207381}, doi = {10.4230/LIPIcs.ITP.2024.10}, annote = {Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12, author = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie}, title = {{A Modular Formalization of Superposition in Isabelle/HOL}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {12:1--12:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12}, URN = {urn:nbn:de:0030-drops-207401}, doi = {10.4230/LIPIcs.ITP.2024.12}, annote = {Keywords: Superposition, verification, first-order logic, higher-order logic} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ekici_et_al:LIPIcs.ITP.2024.13, author = {Ekici, Burak and Yoshida, Nobuko}, title = {{Completeness of Asynchronous Session Tree Subtyping in Coq}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {13:1--13:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.13}, URN = {urn:nbn:de:0030-drops-207418}, doi = {10.4230/LIPIcs.ITP.2024.13}, annote = {Keywords: asynchronous multiparty session types, session trees, subtyping, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dohan Kim. An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kim:LIPIcs.ITP.2024.24, author = {Kim, Dohan}, title = {{An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.24}, URN = {urn:nbn:de:0030-drops-207525}, doi = {10.4230/LIPIcs.ITP.2024.24}, annote = {Keywords: Narrowing, Multiset Narrowing, Unifiability, Reachability} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove. The Power of Counting Steps in Quantitative Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bose_et_al:LIPIcs.CONCUR.2024.13, author = {Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre}, title = {{The Power of Counting Steps in Quantitative Games}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13}, URN = {urn:nbn:de:0030-drops-207852}, doi = {10.4230/LIPIcs.CONCUR.2024.13}, annote = {Keywords: Games on graphs, Markov strategies, quantitative objectives, infinite-state systems} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger. Invariants for One-Counter Automata with Disequality Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2024.17, author = {Chistikov, Dmitry and Leroux, J\'{e}r\^{o}me and Sinclair-Banks, Henry and Waldburger, Nicolas}, title = {{Invariants for One-Counter Automata with Disequality Tests}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {17:1--17:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.17}, URN = {urn:nbn:de:0030-drops-207898}, doi = {10.4230/LIPIcs.CONCUR.2024.17}, annote = {Keywords: Inductive invariant, Vector addition system, One-counter automaton} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Lorenzo Clemente. Weighted Basic Parallel Processes and Combinatorial Enumeration. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clemente:LIPIcs.CONCUR.2024.18, author = {Clemente, Lorenzo}, title = {{Weighted Basic Parallel Processes and Combinatorial Enumeration}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {18:1--18:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.18}, URN = {urn:nbn:de:0030-drops-207903}, doi = {10.4230/LIPIcs.CONCUR.2024.18}, annote = {Keywords: weighted automata, combinatorial enumeration, shuffle, algebraic differential equations, process algebra, basic parallel processes, species of structures} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, and Tim Quatmann. A Spectrum of Approximate Probabilistic Bisimulations. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{spork_et_al:LIPIcs.CONCUR.2024.37, author = {Spork, Timm and Baier, Christel and Katoen, Joost-Pieter and Piribauer, Jakob and Quatmann, Tim}, title = {{A Spectrum of Approximate Probabilistic Bisimulations}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {37:1--37:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.37}, URN = {urn:nbn:de:0030-drops-208099}, doi = {10.4230/LIPIcs.CONCUR.2024.37}, annote = {Keywords: Markov chains, Approximate bisimulation, Abstraction, Model checking} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Zhihan Chen, Peng Lin, Hao Hu, and Shaowei Cai. ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chen_et_al:LIPIcs.CP.2024.5, author = {Chen, Zhihan and Lin, Peng and Hu, Hao and Cai, Shaowei}, title = {{ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.5}, URN = {urn:nbn:de:0030-drops-206900}, doi = {10.4230/LIPIcs.CP.2024.5}, annote = {Keywords: Pseudo-Boolean Optimization, Parallel Solving, Local Search, Scoring Function, Solution Pool} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirović. A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{flippo_et_al:LIPIcs.CP.2024.11, author = {Flippo, Maarten and Sidorov, Konstantin and Marijnissen, Imko and Smits, Jeff and Demirovi\'{c}, Emir}, title = {{A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {11:1--11:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.11}, URN = {urn:nbn:de:0030-drops-206969}, doi = {10.4230/LIPIcs.CP.2024.11}, annote = {Keywords: proof logging, formal verification, constraint programming} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns. Mutational Fuzz Testing for Constraint Modeling Systems. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 29:1-29:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vanroose_et_al:LIPIcs.CP.2024.29, author = {Vanroose, Wout and Bleukx, Ignace and Devriendt, Jo and Tsouros, Dimos and Verhaeghe, H\'{e}l\`{e}ne and Guns, Tias}, title = {{Mutational Fuzz Testing for Constraint Modeling Systems}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {29:1--29:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.29}, URN = {urn:nbn:de:0030-drops-207149}, doi = {10.4230/LIPIcs.CP.2024.29}, annote = {Keywords: fuzz testing, Constraint modeling language, bugs, mutational testing, modeling, constraint reformulation} }
Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bonchi_et_al:LIPIcs.MFCS.2024.30, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide}, title = {{When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-335-5}, ISSN = {1868-8969}, year = {2024}, volume = {306}, editor = {Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.30}, URN = {urn:nbn:de:0030-drops-205867}, doi = {10.4230/LIPIcs.MFCS.2024.30}, annote = {Keywords: relational algebra, hyperdoctrines, cartesian bicategories, string diagrams} }
Feedback for Dagstuhl Publishing