6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1-634, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Paul Downen and Zena M. Ariola. Duality in Action (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1:1-1:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Nao Hirokawa. Completion and Reduction Orders (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Sam Staton. Some Formal Structures in Probability (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Jakob Grue Simonsen. The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Rick Statman. Church’s Semigroup Is Sq-Universal. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 6:1-6:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Tom de Jong and Martín Hötzel Escardó. Predicative Aspects of Order Theory in Univalent Foundations. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Zeinab Galal. A Bicategorical Model for Finite Nondeterminism. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A Functional Abstraction of Typed Invocation Contexts. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Didier Galmiche, Marta Gawek, and Daniel Méry. Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Anupam Das and Alex A. Rice. New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Maika Fujii and Kenichi Asai. Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Lison Blondeau-Patissier and Pierre Clairambault. Positional Injectivity for Innocent Strategies. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Dohan Kim and Christopher Lynch. An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-Deterministic Functions as Non-Deterministic Processes. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Ugo Dal Lago and Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Vincent van Oostrom. Z; Syntax-Free Developments. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Cristina Matache, Sean Moss, and Sam Staton. Recursion and Sequentiality in Categories of Sheaves. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Pieter Hofstra, Jason Parker, and Philip J. Scott. Polymorphic Automorphisms and the Picard Group. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Paolo Pistone and Luca Tranchini. What’s Decidable About (Atomic) Polymorphism?. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra Encoding for Efficient Minimization. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Nathanael Arkor and Dylan McDermott. Abstract Clones for Abstract Syntax. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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-dev.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} }
Feedback for Dagstuhl Publishing