@Proceedings{gaboardi_et_al:LIPIcs.FSCD.2023, title = {{LIPIcs, Volume 260, FSCD 2023, Complete Volume}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {1--658}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023}, URN = {urn:nbn:de:0030-drops-179830}, doi = {10.4230/LIPIcs.FSCD.2023}, annote = {Keywords: LIPIcs, Volume 260, FSCD 2023, Complete Volume} } @InProceedings{gaboardi_et_al:LIPIcs.FSCD.2023.0, author = {Gaboardi, Marco and van Raamsdonk, Femke}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {0:i--0:xviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.0}, URN = {urn:nbn:de:0030-drops-179849}, doi = {10.4230/LIPIcs.FSCD.2023.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{fernandez:LIPIcs.FSCD.2023.1, author = {Fern\'{a}ndez, Maribel}, title = {{Nominal Techniques for Software Specification and Verification}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.1}, URN = {urn:nbn:de:0030-drops-179855}, doi = {10.4230/LIPIcs.FSCD.2023.1}, annote = {Keywords: Binding operator, Nominal Logic, Nominal Rewriting, Unification, Equational Theories, Type Systems} } @InProceedings{jamnik:LIPIcs.FSCD.2023.2, author = {Jamnik, Mateja}, title = {{How Can We Make Trustworthy AI?}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.2}, URN = {urn:nbn:de:0030-drops-179869}, doi = {10.4230/LIPIcs.FSCD.2023.2}, annote = {Keywords: AI, human-centric computing, knowledge representation, reasoning, machine learning} } @InProceedings{manzonetto:LIPIcs.FSCD.2023.3, author = {Manzonetto, Giulio}, title = {{A Lambda Calculus Satellite}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {3:1--3:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.3}, URN = {urn:nbn:de:0030-drops-179878}, doi = {10.4230/LIPIcs.FSCD.2023.3}, annote = {Keywords: \lambda-calculus, rewriting, denotational models, equational theories} } @InProceedings{yamada:LIPIcs.FSCD.2023.4, author = {Yamada, Akihisa}, title = {{Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {4:1--4:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.4}, URN = {urn:nbn:de:0030-drops-179882}, doi = {10.4230/LIPIcs.FSCD.2023.4}, annote = {Keywords: Term rewriting, Termination, Isabelle/HOL, Competition} } @InProceedings{uemura:LIPIcs.FSCD.2023.5, author = {Uemura, Taichi}, title = {{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.5}, URN = {urn:nbn:de:0030-drops-179897}, doi = {10.4230/LIPIcs.FSCD.2023.5}, annote = {Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation} } @InProceedings{vanderweide:LIPIcs.FSCD.2023.6, author = {van der Weide, Niels}, title = {{The Formal Theory of Monads, Univalently}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {6:1--6:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.6}, URN = {urn:nbn:de:0030-drops-179904}, doi = {10.4230/LIPIcs.FSCD.2023.6}, annote = {Keywords: bicategory theory, univalent foundations, formalization, monads, Coq} } @InProceedings{losekoot_et_al:LIPIcs.FSCD.2023.7, author = {Losekoot, Th\'{e}o and Genet, Thomas and Jensen, Thomas}, title = {{Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {7:1--7:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.7}, URN = {urn:nbn:de:0030-drops-179915}, doi = {10.4230/LIPIcs.FSCD.2023.7}, annote = {Keywords: Formal verification, Tree automata, Constrained Horn Clauses, Model inference, Relational properties, Algebraic datatypes} } @InProceedings{ehrhard_et_al:LIPIcs.FSCD.2023.8, author = {Ehrhard, Thomas and Faggian, Claudia and Pagani, Michele}, title = {{The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.8}, URN = {urn:nbn:de:0030-drops-179926}, doi = {10.4230/LIPIcs.FSCD.2023.8}, annote = {Keywords: Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming} } @InProceedings{ivanov:LIPIcs.FSCD.2023.9, author = {Ivanov, Ievgen}, title = {{Generalized Newman’s Lemma for Discrete and Continuous Systems}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.9}, URN = {urn:nbn:de:0030-drops-179936}, doi = {10.4230/LIPIcs.FSCD.2023.9}, annote = {Keywords: abstract rewriting system, confluence, discrete-continuous systems, proof assistant, formal proof} } @InProceedings{kudasov:LIPIcs.FSCD.2023.10, author = {Kudasov, Nikolai}, title = {{E-Unification for Second-Order Abstract Syntax}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {10:1--10:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10}, URN = {urn:nbn:de:0030-drops-179944}, doi = {10.4230/LIPIcs.FSCD.2023.10}, annote = {Keywords: E-unification, higher-order unification, second-order abstract syntax} } @InProceedings{barenbaum_et_al:LIPIcs.FSCD.2023.11, author = {Barenbaum, Pablo and Sottile, Cristian}, title = {{Two Decreasing Measures for Simply Typed \lambda-Terms}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.11}, URN = {urn:nbn:de:0030-drops-179956}, doi = {10.4230/LIPIcs.FSCD.2023.11}, annote = {Keywords: Lambda Calculus, Rewriting, Termination, Strong Normalization, Simple Types} } @InProceedings{hirokawa_et_al:LIPIcs.FSCD.2023.12, author = {Hirokawa, Nao and Middeldorp, Aart}, title = {{Hydra Battles and AC Termination}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.12}, URN = {urn:nbn:de:0030-drops-179965}, doi = {10.4230/LIPIcs.FSCD.2023.12}, annote = {Keywords: battle of Hercules and Hydra, term rewriting, termination} } @InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2023.13, author = {Blondeau-Patissier, Lison and Clairambault, Pierre and Vaux Auclair, Lionel}, title = {{Strategies as Resource Terms, and Their Categorical Semantics}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {13:1--13:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.13}, URN = {urn:nbn:de:0030-drops-179976}, doi = {10.4230/LIPIcs.FSCD.2023.13}, annote = {Keywords: Resource calculus, Game semantics, Categorical semantics} } @InProceedings{ghica_et_al:LIPIcs.FSCD.2023.14, author = {Ghica, Dan R. and Kaye, George}, title = {{Rewriting Modulo Traced Comonoid Structure}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {14:1--14:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.14}, URN = {urn:nbn:de:0030-drops-179983}, doi = {10.4230/LIPIcs.FSCD.2023.14}, annote = {Keywords: symmetric traced monoidal categories, string diagrams, graph rewriting, comonoid structure, double pushout rewriting} } @InProceedings{kop_et_al:LIPIcs.FSCD.2023.15, author = {Kop, Cynthia and Vale, Deivid}, title = {{Cost-Size Semantics for Call-By-Value Higher-Order Rewriting}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {15:1--15:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.15}, URN = {urn:nbn:de:0030-drops-179993}, doi = {10.4230/LIPIcs.FSCD.2023.15}, annote = {Keywords: Call-by-Value Evaluation, Complexity Theory, Higher-Order Rewriting} } @InProceedings{mimram:LIPIcs.FSCD.2023.16, author = {Mimram, Samuel}, title = {{Categorical Coherence from Term Rewriting Systems}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.16}, URN = {urn:nbn:de:0030-drops-180009}, doi = {10.4230/LIPIcs.FSCD.2023.16}, annote = {Keywords: coherence, rewriting system, Lawvere theory} } @InProceedings{behr_et_al:LIPIcs.FSCD.2023.17, author = {Behr, Nicolas and Melli\`{e}s, Paul-Andr\'{e} and Zeilberger, Noam}, title = {{Convolution Products on Double Categories and Categorification of Rule Algebras}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {17:1--17:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17}, URN = {urn:nbn:de:0030-drops-180017}, doi = {10.4230/LIPIcs.FSCD.2023.17}, annote = {Keywords: Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra} } @InProceedings{bocquet_et_al:LIPIcs.FSCD.2023.18, author = {Bocquet, Rafa\"{e}l and Kaposi, Ambrus and Sattler, Christian}, title = {{For the Metatheory of Type Theory, Internal Sconing Is Enough}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {18:1--18:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.18}, URN = {urn:nbn:de:0030-drops-180029}, doi = {10.4230/LIPIcs.FSCD.2023.18}, annote = {Keywords: type theory, presheaves, canonicity, normalization, sconing, gluing} } @InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2023.19, author = {Esp{\'\i}rito Santo, Jos\'{e} and Mendes, Filipa}, title = {{The Logical Essence of Compiling with Continuations}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {19:1--19:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.19}, URN = {urn:nbn:de:0030-drops-180036}, doi = {10.4230/LIPIcs.FSCD.2023.19}, annote = {Keywords: Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form} } @InProceedings{dallago_et_al:LIPIcs.FSCD.2023.20, author = {Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo}, title = {{On the Lattice of Program Metrics}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.20}, URN = {urn:nbn:de:0030-drops-180049}, doi = {10.4230/LIPIcs.FSCD.2023.20}, annote = {Keywords: Metrics, Lambda Calculus, Linear Types} } @InProceedings{breuvart_et_al:LIPIcs.FSCD.2023.21, author = {Breuvart, Flavien and Kerjean, Marie and Mirwasser, Simon}, title = {{Unifying Graded Linear Logic and Differential Operators}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {21:1--21:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.21}, URN = {urn:nbn:de:0030-drops-180052}, doi = {10.4230/LIPIcs.FSCD.2023.21}, annote = {Keywords: Linear Logic, Denotational Semantics, Functional Analysis, Graded Logic} } @InProceedings{frontull_et_al:LIPIcs.FSCD.2023.22, author = {Frontull, Samuel and Moser, Georg and van Oostrom, Vincent}, title = {{\alpha-Avoidance}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {22:1--22:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.22}, URN = {urn:nbn:de:0030-drops-180068}, doi = {10.4230/LIPIcs.FSCD.2023.22}, annote = {Keywords: \lambda-calculus, variable capture, \alpha-conversion, developments, safe \lambda-calculus, undecidability} } @InProceedings{cerrito_et_al:LIPIcs.FSCD.2023.23, author = {Cerrito, Serenella and Goranko, Valentin and Paillocher, Sophie}, title = {{Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {23:1--23:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.23}, URN = {urn:nbn:de:0030-drops-180075}, doi = {10.4230/LIPIcs.FSCD.2023.23}, annote = {Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux} } @InProceedings{altenkirch_et_al:LIPIcs.FSCD.2023.24, author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s}, title = {{Combinatory Logic and Lambda Calculus Are Equal, Algebraically}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24}, URN = {urn:nbn:de:0030-drops-180086}, doi = {10.4230/LIPIcs.FSCD.2023.24}, annote = {Keywords: Combinatory logic, lambda calculus, quotient inductive types, Cubical Agda} } @InProceedings{dagnino_et_al:LIPIcs.FSCD.2023.25, author = {Dagnino, Francesco and Pasquali, Fabio}, title = {{Quotients and Extensionality in Relational Doctrines}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {25:1--25:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.25}, URN = {urn:nbn:de:0030-drops-180090}, doi = {10.4230/LIPIcs.FSCD.2023.25}, annote = {Keywords: Quantitative Reasoning, Calculus of Relations, Hyperdoctrines, Metric Spaces} } @InProceedings{diguardia_et_al:LIPIcs.FSCD.2023.26, author = {Di Guardia, R\'{e}mi and Laurent, Olivier}, title = {{Type Isomorphisms for Multiplicative-Additive Linear Logic}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {26:1--26:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.26}, URN = {urn:nbn:de:0030-drops-180103}, doi = {10.4230/LIPIcs.FSCD.2023.26}, annote = {Keywords: Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products} } @InProceedings{das_et_al:LIPIcs.FSCD.2023.27, author = {Das, Anupam and Melgaard, Lukas}, title = {{Cyclic Proofs for Arithmetical Inductive Definitions}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {27:1--27:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.27}, URN = {urn:nbn:de:0030-drops-180119}, doi = {10.4230/LIPIcs.FSCD.2023.27}, annote = {Keywords: cyclic proofs, inductive definitions, arithmetic, fixed points, proof theory} } @InProceedings{beffara_et_al:LIPIcs.FSCD.2023.28, author = {Beffara, Emmanuel and Castro, F\'{e}lix and Guillermo, Mauricio and Miquey, \'{E}tienne}, title = {{Concurrent Realizability on Conjunctive Structures}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {28:1--28:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.28}, URN = {urn:nbn:de:0030-drops-180124}, doi = {10.4230/LIPIcs.FSCD.2023.28}, annote = {Keywords: Realizability, Process Algebras, Concurrent Processes, Linear Logic} } @InProceedings{pautasso_et_al:LIPIcs.FSCD.2023.29, author = {Pautasso, Daniele and Ronchi Della Rocca, Simona}, title = {{A Quantitative Version of Simple Types}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {29:1--29:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.29}, URN = {urn:nbn:de:0030-drops-180137}, doi = {10.4230/LIPIcs.FSCD.2023.29}, annote = {Keywords: \lambda-calculus, intersection types, unification} } @InProceedings{dwyersatterfield_et_al:LIPIcs.FSCD.2023.30, author = {Dwyer Satterfield, Saraid and Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe}, title = {{Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.30}, URN = {urn:nbn:de:0030-drops-180148}, doi = {10.4230/LIPIcs.FSCD.2023.30}, annote = {Keywords: Term rewriting, security protocols, verification} } @InProceedings{galmiche_et_al:LIPIcs.FSCD.2023.31, author = {Galmiche, Didier and M\'{e}ry, Daniel}, title = {{Labelled Tableaux for Linear Time Bunched Implication Logic}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.31}, URN = {urn:nbn:de:0030-drops-180159}, doi = {10.4230/LIPIcs.FSCD.2023.31}, annote = {Keywords: Temporal Logic, Bunched Implication Logic, Labelled Deduction, Tableaux} } @InProceedings{blot:LIPIcs.FSCD.2023.32, author = {Blot, Valentin}, title = {{Diller-Nahm Bar Recursion}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {32:1--32:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.32}, URN = {urn:nbn:de:0030-drops-180164}, doi = {10.4230/LIPIcs.FSCD.2023.32}, annote = {Keywords: Dialectica, Bar recursion} } @InProceedings{laird:LIPIcs.FSCD.2023.33, author = {Laird, James}, title = {{Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.33}, URN = {urn:nbn:de:0030-drops-180171}, doi = {10.4230/LIPIcs.FSCD.2023.33}, annote = {Keywords: Subtyping, Bounded Polymorphism, Game Semantics, Dinaturality} } @InProceedings{goncharov:LIPIcs.FSCD.2023.34, author = {Goncharov, Sergey}, title = {{Representing Guardedness in Call-By-Value}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {34:1--34:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.34}, URN = {urn:nbn:de:0030-drops-180181}, doi = {10.4230/LIPIcs.FSCD.2023.34}, annote = {Keywords: Fine-grain call-by-value, Abstract guardedness, Freyd category, Kleisli category, Elgot iteration} }