@Proceedings{kobayashi:LIPIcs.FSCD.2021, title = {{LIPIcs, Volume 195, FSCD 2021, Complete Volume}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {1--634}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021}, URN = {urn:nbn:de:0030-drops-142371}, doi = {10.4230/LIPIcs.FSCD.2021}, annote = {Keywords: LIPIcs, Volume 195, FSCD 2021, Complete Volume} } @InProceedings{kobayashi:LIPIcs.FSCD.2021.0, author = {Kobayashi, Naoki}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {0:i--0:xvi}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.0}, URN = {urn:nbn:de:0030-drops-142382}, doi = {10.4230/LIPIcs.FSCD.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{downen_et_al:LIPIcs.FSCD.2021.1, author = {Downen, Paul and Ariola, Zena M.}, title = {{Duality in Action}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {1:1--1:32}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.1}, URN = {urn:nbn:de:0030-drops-142390}, doi = {10.4230/LIPIcs.FSCD.2021.1}, annote = {Keywords: Duality, Logic, Curry-Howard, Sequent Calculus, Rewriting, Compilation} } @InProceedings{hirokawa:LIPIcs.FSCD.2021.2, author = {Hirokawa, Nao}, title = {{Completion and Reduction Orders}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {2:1--2:9}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.2}, URN = {urn:nbn:de:0030-drops-142403}, doi = {10.4230/LIPIcs.FSCD.2021.2}, annote = {Keywords: term rewriting, completion, reduction order} } @InProceedings{pimentel_et_al:LIPIcs.FSCD.2021.3, author = {Pimentel, Elaine and Olarte, Carlos and Nigam, Vivek}, title = {{Process-As-Formula Interpretation: A Substructural Multimodal View}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {3:1--3:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.3}, URN = {urn:nbn:de:0030-drops-142414}, doi = {10.4230/LIPIcs.FSCD.2021.3}, annote = {Keywords: Linear logic, proof theory, process calculi} } @InProceedings{staton:LIPIcs.FSCD.2021.4, author = {Staton, Sam}, title = {{Some Formal Structures in Probability}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {4:1--4:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.4}, URN = {urn:nbn:de:0030-drops-142421}, doi = {10.4230/LIPIcs.FSCD.2021.4}, annote = {Keywords: Probabilistic programming} } @InProceedings{simonsen:LIPIcs.FSCD.2021.5, author = {Simonsen, Jakob Grue}, title = {{The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.5}, URN = {urn:nbn:de:0030-drops-142439}, doi = {10.4230/LIPIcs.FSCD.2021.5}, annote = {Keywords: Constructor term rewriting, Chomsky Hierarchy, Implicit Complexity} } @InProceedings{statman:LIPIcs.FSCD.2021.6, author = {Statman, Rick}, title = {{Church’s Semigroup Is Sq-Universal}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {6:1--6:6}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.6}, URN = {urn:nbn:de:0030-drops-142448}, doi = {10.4230/LIPIcs.FSCD.2021.6}, annote = {Keywords: lambda calculus, Church’s semigroup, sq-universal} } @InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7, author = {Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona}, title = {{Call-By-Value, Again!}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {7:1--7:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.7}, URN = {urn:nbn:de:0030-drops-142458}, doi = {10.4230/LIPIcs.FSCD.2021.7}, annote = {Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation} } @InProceedings{dejong_et_al:LIPIcs.FSCD.2021.8, author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel}, title = {{Predicative Aspects of Order Theory in Univalent Foundations}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.8}, URN = {urn:nbn:de:0030-drops-142461}, doi = {10.4230/LIPIcs.FSCD.2021.8}, annote = {Keywords: order theory, constructivity, predicativity, univalent foundations} } @InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9, author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume}, title = {{A Strong Call-By-Need Calculus}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {9:1--9:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9}, URN = {urn:nbn:de:0030-drops-142477}, doi = {10.4230/LIPIcs.FSCD.2021.9}, annote = {Keywords: strong reduction, call-by-need, evaluation strategy, normalization} } @InProceedings{galal:LIPIcs.FSCD.2021.10, author = {Galal, Zeinab}, title = {{A Bicategorical Model for Finite Nondeterminism}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {10:1--10:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.10}, URN = {urn:nbn:de:0030-drops-142487}, doi = {10.4230/LIPIcs.FSCD.2021.10}, annote = {Keywords: Differential linear logic, Species of structures, Finiteness, Bicategorical semantics} } @InProceedings{saotome_et_al:LIPIcs.FSCD.2021.11, author = {Saotome, Kenji and Nakazawa, Koji and Kimura, Daisuke}, title = {{Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {11:1--11:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.11}, URN = {urn:nbn:de:0030-drops-142494}, doi = {10.4230/LIPIcs.FSCD.2021.11}, annote = {Keywords: cyclic proofs, cut-elimination, bunched logic, separation logic, linear logic} } @InProceedings{cong_et_al:LIPIcs.FSCD.2021.12, author = {Cong, Youyou and Ishio, Chiaki and Honda, Kaho and Asai, Kenichi}, title = {{A Functional Abstraction of Typed Invocation Contexts}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {12:1--12:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.12}, URN = {urn:nbn:de:0030-drops-142507}, doi = {10.4230/LIPIcs.FSCD.2021.12}, annote = {Keywords: delimited continuations, control operators, control and prompt, CPS translation, type system} } @InProceedings{galmiche_et_al:LIPIcs.FSCD.2021.13, author = {Galmiche, Didier and Gawek, Marta and M\'{e}ry, Daniel}, title = {{Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {13:1--13:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.13}, URN = {urn:nbn:de:0030-drops-142516}, doi = {10.4230/LIPIcs.FSCD.2021.13}, annote = {Keywords: Algebraic Semantics, Beth Models, Labelled Deduction, Intuitionistic Logic} } @InProceedings{das_et_al:LIPIcs.FSCD.2021.14, author = {Das, Anupam and Rice, Alex A.}, title = {{New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {14:1--14:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.14}, URN = {urn:nbn:de:0030-drops-142525}, doi = {10.4230/LIPIcs.FSCD.2021.14}, annote = {Keywords: rewriting, linear inference, proof theory, linear logic, implementation} } @InProceedings{kapur:LIPIcs.FSCD.2021.15, author = {Kapur, Deepak}, title = {{A Modular Associative Commutative (AC) Congruence Closure Algorithm}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {15:1--15:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.15}, URN = {urn:nbn:de:0030-drops-142530}, doi = {10.4230/LIPIcs.FSCD.2021.15}, annote = {Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories} } @InProceedings{fujii_et_al:LIPIcs.FSCD.2021.16, author = {Fujii, Maika and Asai, Kenichi}, title = {{Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {16:1--16:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.16}, URN = {urn:nbn:de:0030-drops-142547}, doi = {10.4230/LIPIcs.FSCD.2021.16}, annote = {Keywords: delimited-control operators, functional derivation, CPS transformation, defunctionalization, abstract machine, virtual machine} } @InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2021.17, author = {Blondeau-Patissier, Lison and Clairambault, Pierre}, title = {{Positional Injectivity for Innocent Strategies}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {17:1--17:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.17}, URN = {urn:nbn:de:0030-drops-142555}, doi = {10.4230/LIPIcs.FSCD.2021.17}, annote = {Keywords: Game Semantics, Innocence, Relational Semantics, Positionality} } @InProceedings{larcheywendling:LIPIcs.FSCD.2021.18, author = {Larchey-Wendling, Dominique}, title = {{Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.18}, URN = {urn:nbn:de:0030-drops-142568}, doi = {10.4230/LIPIcs.FSCD.2021.18}, annote = {Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq} } @InProceedings{kim_et_al:LIPIcs.FSCD.2021.19, author = {Kim, Dohan and Lynch, Christopher}, title = {{An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {19:1--19:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.19}, URN = {urn:nbn:de:0030-drops-142572}, doi = {10.4230/LIPIcs.FSCD.2021.19}, annote = {Keywords: Recursive Path Ordering, Permutation Equation, Permutation Group, Rewrite System, Completion, Ground Completion} } @InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20, author = {Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois}, title = {{Some Axioms for Mathematics}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20}, URN = {urn:nbn:de:0030-drops-142581}, doi = {10.4230/LIPIcs.FSCD.2021.20}, annote = {Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty} } @InProceedings{paulus_et_al:LIPIcs.FSCD.2021.21, author = {Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.}, title = {{Non-Deterministic Functions as Non-Deterministic Processes}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {21:1--21:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.21}, URN = {urn:nbn:de:0030-drops-142598}, doi = {10.4230/LIPIcs.FSCD.2021.21}, annote = {Keywords: Resource calculi, \pi-calculus, intersection types, session types, linear logic} } @InProceedings{veltri:LIPIcs.FSCD.2021.22, author = {Veltri, Niccol\`{o}}, title = {{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22}, URN = {urn:nbn:de:0030-drops-142601}, doi = {10.4230/LIPIcs.FSCD.2021.22}, annote = {Keywords: type theory, finite powerset, final coalgebra, Cubical Agda} } @InProceedings{dallago_et_al:LIPIcs.FSCD.2021.23, author = {Dal Lago, Ugo and Gavazzo, Francesco}, title = {{Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {23:1--23:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.23}, URN = {urn:nbn:de:0030-drops-142618}, doi = {10.4230/LIPIcs.FSCD.2021.23}, annote = {Keywords: algebraic effects, linearity, program equivalence, full abstraction} } @InProceedings{vanoostrom:LIPIcs.FSCD.2021.24, author = {van Oostrom, Vincent}, title = {{Z; Syntax-Free Developments}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {24:1--24:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.24}, URN = {urn:nbn:de:0030-drops-142620}, doi = {10.4230/LIPIcs.FSCD.2021.24}, annote = {Keywords: rewrite system, confluence, normalisation, recurrence} } @InProceedings{matache_et_al:LIPIcs.FSCD.2021.25, author = {Matache, Cristina and Moss, Sean and Staton, Sam}, title = {{Recursion and Sequentiality in Categories of Sheaves}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {25:1--25:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.25}, URN = {urn:nbn:de:0030-drops-142631}, doi = {10.4230/LIPIcs.FSCD.2021.25}, annote = {Keywords: Denotational semantics, Full abstraction, Recursion, Sheaf toposes, CPOs} } @InProceedings{hofstra_et_al:LIPIcs.FSCD.2021.26, author = {Hofstra, Pieter and Parker, Jason and Scott, Philip J.}, title = {{Polymorphic Automorphisms and the Picard Group}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {26:1--26:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.26}, URN = {urn:nbn:de:0030-drops-142646}, doi = {10.4230/LIPIcs.FSCD.2021.26}, annote = {Keywords: Partial Horn Theories, Monoidal Categories, Definable Automorphisms, Polymorphism, Indeterminates, Normal Forms} } @InProceedings{pistone_et_al:LIPIcs.FSCD.2021.27, author = {Pistone, Paolo and Tranchini, Luca}, title = {{What’s Decidable About (Atomic) Polymorphism?}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {27:1--27:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.27}, URN = {urn:nbn:de:0030-drops-142652}, doi = {10.4230/LIPIcs.FSCD.2021.27}, annote = {Keywords: Atomic System F, Predicative Polymorphism, ML-Polymorphism, Type-Checking, Contextual Equivalence, Free Theorems} } @InProceedings{deifel_et_al:LIPIcs.FSCD.2021.28, author = {Deifel, Hans-Peter and Milius, Stefan and Wi{\ss}mann, Thorsten}, title = {{Coalgebra Encoding for Efficient Minimization}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {28:1--28:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.28}, URN = {urn:nbn:de:0030-drops-142664}, doi = {10.4230/LIPIcs.FSCD.2021.28}, annote = {Keywords: Coalgebra, Partition refinement, Transition systems, Minimization} } @InProceedings{das:LIPIcs.FSCD.2021.29, author = {Das, Anupam}, title = {{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {29:1--29:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.29}, URN = {urn:nbn:de:0030-drops-142678}, doi = {10.4230/LIPIcs.FSCD.2021.29}, annote = {Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures} } @InProceedings{arkor_et_al:LIPIcs.FSCD.2021.30, author = {Arkor, Nathanael and McDermott, Dylan}, title = {{Abstract Clones for Abstract Syntax}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.30}, URN = {urn:nbn:de:0030-drops-142686}, doi = {10.4230/LIPIcs.FSCD.2021.30}, annote = {Keywords: simple type theories, abstract clones, second-order abstract syntax, substitution, variable binding, presentations, free algebras, induction, logical relations} } @InProceedings{kop_et_al:LIPIcs.FSCD.2021.31, author = {Kop, Cynthia and Vale, Deivid}, title = {{Tuple Interpretations for Higher-Order Complexity}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {31:1--31:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.31}, URN = {urn:nbn:de:0030-drops-142692}, doi = {10.4230/LIPIcs.FSCD.2021.31}, annote = {Keywords: Complexity, higher-order term rewriting, many-sorted term rewriting, polynomial interpretations, weakly monotonic algebras} } @InProceedings{sakayori_et_al:LIPIcs.FSCD.2021.32, author = {Sakayori, Ken and Tsukada, Takeshi}, title = {{Output Without Delay: A \pi-Calculus Compatible with Categorical Semantics}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {32:1--32:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.32}, URN = {urn:nbn:de:0030-drops-142705}, doi = {10.4230/LIPIcs.FSCD.2021.32}, annote = {Keywords: \pi-calculus, categorical semantics, linear approximation} }