@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} }
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing