@Proceedings{kirchner:LIPIcs.FSCD.2018, title = {{LIPIcs, Volume 108, FSCD'18, Complete Volume}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018}, URN = {urn:nbn:de:0030-drops-92819}, doi = {10.4230/LIPIcs.FSCD.2018}, annote = {Keywords: Theory of computation, Models of computation, Formal languages and automata theory, Logic, Semantics and reasoning, Software and its engineering} } @InProceedings{kirchner:LIPIcs.FSCD.2018.0, author = {Kirchner, H\'{e}l\`{e}ne}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.0}, URN = {urn:nbn:de:0030-drops-91706}, doi = {10.4230/LIPIcs.FSCD.2018.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{delaune:LIPIcs.FSCD.2018.1, author = {Delaune, St\'{e}phanie}, title = {{Analysing Privacy-Type Properties in Cryptographic Protocols}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {1:1--1:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.1}, URN = {urn:nbn:de:0030-drops-91715}, doi = {10.4230/LIPIcs.FSCD.2018.1}, annote = {Keywords: cryptographic protocols, symbolic models, privacy-related properties, behavioural equivalence} } @InProceedings{rosu:LIPIcs.FSCD.2018.2, author = {Rosu, Grigore}, title = {{Formal Design, Implementation and Verification of Blockchain Languages}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {2:1--2:6}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.2}, URN = {urn:nbn:de:0030-drops-91722}, doi = {10.4230/LIPIcs.FSCD.2018.2}, annote = {Keywords: Formal semantics, Program verification, Blockchain} } @InProceedings{selinger:LIPIcs.FSCD.2018.3, author = {Selinger, Peter}, title = {{Challenges in Quantum Programming Languages}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {3:1--3:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.3}, URN = {urn:nbn:de:0030-drops-91730}, doi = {10.4230/LIPIcs.FSCD.2018.3}, annote = {Keywords: Quantum programming languages} } @InProceedings{vignudelli:LIPIcs.FSCD.2018.4, author = {Vignudelli, Valeria}, title = {{Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {4:1--4:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.4}, URN = {urn:nbn:de:0030-drops-91749}, doi = {10.4230/LIPIcs.FSCD.2018.4}, annote = {Keywords: Lambda Calculus, Contextual Equivalence, Bisimulation, Probabilistic Programming Languages} } @InProceedings{alves_et_al:LIPIcs.FSCD.2018.5, author = {Alves, Sandra and Broda, Sabine}, title = {{A Unifying Framework for Type Inhabitation}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.5}, URN = {urn:nbn:de:0030-drops-91758}, doi = {10.4230/LIPIcs.FSCD.2018.5}, annote = {Keywords: simple types, type inhabitation, rewriting, PSPACE} } @InProceedings{andrianarivelo_et_al:LIPIcs.FSCD.2018.6, author = {Andrianarivelo, Nirina and R\'{e}ty, Pierre}, title = {{Confluence of Prefix-Constrained Rewrite Systems}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {6:1--6:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.6}, URN = {urn:nbn:de:0030-drops-91762}, doi = {10.4230/LIPIcs.FSCD.2018.6}, annote = {Keywords: prefix-constrained term rewriting, confluence, critical pair} } @InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2018.7, author = {Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele}, title = {{Fixed-Point Constraints for Nominal Equational Unification}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {7:1--7:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7}, URN = {urn:nbn:de:0030-drops-91777}, doi = {10.4230/LIPIcs.FSCD.2018.7}, annote = {Keywords: nominal terms, fixed-point equations, nominal unification, equational theories} } @InProceedings{bahr:LIPIcs.FSCD.2018.8, author = {Bahr, Patrick}, title = {{Strict Ideal Completions of the Lambda Calculus}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.8}, URN = {urn:nbn:de:0030-drops-91787}, doi = {10.4230/LIPIcs.FSCD.2018.8}, annote = {Keywords: lambda calculus, infinitary rewriting, B\"{o}hm trees, meaningless terms, confluence} } @InProceedings{baumgartner_et_al:LIPIcs.FSCD.2018.9, author = {Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu}, title = {{Term-Graph Anti-Unification}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.9}, URN = {urn:nbn:de:0030-drops-91797}, doi = {10.4230/LIPIcs.FSCD.2018.9}, annote = {Keywords: Cyclic term-graps, anti-unification, least general generalization} } @InProceedings{bellin_et_al:LIPIcs.FSCD.2018.10, author = {Bellin, Gianluigi and Heijltjes, Willem B.}, title = {{Proof Nets for Bi-Intuitionistic Linear Logic}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.10}, URN = {urn:nbn:de:0030-drops-91800}, doi = {10.4230/LIPIcs.FSCD.2018.10}, annote = {Keywords: proof nets, intuitionistic linear logic, contractibility, linear logic} } @InProceedings{bendkowski_et_al:LIPIcs.FSCD.2018.11, author = {Bendkowski, Maciej and Lescanne, Pierre}, title = {{Counting Environments and Closures}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {11:1--11:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.11}, URN = {urn:nbn:de:0030-drops-91817}, doi = {10.4230/LIPIcs.FSCD.2018.11}, annote = {Keywords: lambda-calculus, combinatorics, functional programming, mathematical analysis, complexity} } @InProceedings{cerna_et_al:LIPIcs.FSCD.2018.12, author = {Cerna, David M. and Kutsia, Temur}, title = {{Higher-Order Equational Pattern Anti-Unification}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {12:1--12:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.12}, URN = {urn:nbn:de:0030-drops-91826}, doi = {10.4230/LIPIcs.FSCD.2018.12}, annote = {Keywords: Simply typed lambda calculus, anti-unification, equational theories} } @InProceedings{czajka:LIPIcs.FSCD.2018.13, author = {Czajka, Lukasz}, title = {{Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {13:1--13:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.13}, URN = {urn:nbn:de:0030-drops-91831}, doi = {10.4230/LIPIcs.FSCD.2018.13}, annote = {Keywords: LOGSPACE, implicit complexity, term rewriting, infinitary rewriting, streams} } @InProceedings{endrullis_et_al:LIPIcs.FSCD.2018.14, author = {Endrullis, J\"{o}rg and Klop, Jan Willem and Overbeek, Roy}, title = {{Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {14:1--14:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.14}, URN = {urn:nbn:de:0030-drops-91848}, doi = {10.4230/LIPIcs.FSCD.2018.14}, annote = {Keywords: confluence, decreasing diagrams, weak diamond property} } @InProceedings{forest_et_al:LIPIcs.FSCD.2018.15, author = {Forest, Simon and Mimram, Samuel}, title = {{Coherence of Gray Categories via Rewriting}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.15}, URN = {urn:nbn:de:0030-drops-91855}, doi = {10.4230/LIPIcs.FSCD.2018.15}, annote = {Keywords: rewriting, coherence, Gray category, polygraph, pseudomonoid, precategory} } @InProceedings{genet:LIPIcs.FSCD.2018.16, author = {Genet, Thomas}, title = {{Completeness of Tree Automata Completion}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {16:1--16:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.16}, URN = {urn:nbn:de:0030-drops-91868}, doi = {10.4230/LIPIcs.FSCD.2018.16}, annote = {Keywords: term rewriting systems, regularity preservation, over-approximation, completeness, tree automata, tree automata completion} } @InProceedings{hadzihasanovic_et_al:LIPIcs.FSCD.2018.17, author = {Hadzihasanovic, Amar and de Felice, Giovanni and Ng, Kang Feng}, title = {{A Diagrammatic Axiomatisation of Fermionic Quantum Circuits}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {17:1--17:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.17}, URN = {urn:nbn:de:0030-drops-91873}, doi = {10.4230/LIPIcs.FSCD.2018.17}, annote = {Keywords: Fermionic Quantum Computing, String Diagrams, Categorical Quantum Mechanics} } @InProceedings{ikebuchi_et_al:LIPIcs.FSCD.2018.18, author = {Ikebuchi, Mirai and Nakano, Keisuke}, title = {{On Repetitive Right Application of B-Terms}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {18:1--18:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.18}, URN = {urn:nbn:de:0030-drops-91882}, doi = {10.4230/LIPIcs.FSCD.2018.18}, annote = {Keywords: Combinatory logic, B combinator, Lambda calculus} } @InProceedings{jacobrao_et_al:LIPIcs.FSCD.2018.19, author = {Jacob-Rao, Rohan and Pientka, Brigitte and Thibodeau, David}, title = {{Index-Stratified Types}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {19:1--19:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.19}, URN = {urn:nbn:de:0030-drops-91891}, doi = {10.4230/LIPIcs.FSCD.2018.19}, annote = {Keywords: Indexed types, (co)recursive types, logical relations} } @InProceedings{kaposi_et_al:LIPIcs.FSCD.2018.20, author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s}, title = {{A Syntax for Higher Inductive-Inductive Types}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.20}, URN = {urn:nbn:de:0030-drops-91906}, doi = {10.4230/LIPIcs.FSCD.2018.20}, annote = {Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations} } @InProceedings{lemay:LIPIcs.FSCD.2018.21, author = {Lemay, Jean-Simon Pacaud}, title = {{Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {21:1--21:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.21}, URN = {urn:nbn:de:0030-drops-91911}, doi = {10.4230/LIPIcs.FSCD.2018.21}, annote = {Keywords: Mixed Distributive Laws, Coalgebra Modalities, Linear Categories, Bimonads, Differential Categories} } @InProceedings{licata_et_al:LIPIcs.FSCD.2018.22, author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas}, title = {{Internal Universes in Models of Homotopy Type Theory}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {22:1--22:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.22}, URN = {urn:nbn:de:0030-drops-91929}, doi = {10.4230/LIPIcs.FSCD.2018.22}, annote = {Keywords: cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes} } @InProceedings{mannaa_et_al:LIPIcs.FSCD.2018.23, author = {Mannaa, Bassel and M{\o}gelberg, Rasmus Ejlers}, title = {{The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {23:1--23:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.23}, URN = {urn:nbn:de:0030-drops-91938}, doi = {10.4230/LIPIcs.FSCD.2018.23}, annote = {Keywords: Guarded type theory, Coinduction, Presheaf model, Clocked type theory, Dependent adjunction} } @InProceedings{new_et_al:LIPIcs.FSCD.2018.24, author = {New, Max S. and Licata, Daniel R.}, title = {{Call-by-Name Gradual Type Theory}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {24:1--24:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.24}, URN = {urn:nbn:de:0030-drops-91944}, doi = {10.4230/LIPIcs.FSCD.2018.24}, annote = {Keywords: Gradual Typing, Type Systems, Program Logics, Category Theory, Denotational Semantics} } @InProceedings{nguyen:LIPIcs.FSCD.2018.25, author = {Nguyen, L\^{e} Th\`{a}nh Dung}, title = {{Unique perfect matchings and proof nets}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {25:1--25:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.25}, URN = {urn:nbn:de:0030-drops-91957}, doi = {10.4230/LIPIcs.FSCD.2018.25}, annote = {Keywords: correctness criteria, matching algorithms} } @InProceedings{nishida_et_al:LIPIcs.FSCD.2018.26, author = {Nishida, Naoki and Maeda, Yuya}, title = {{Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.26}, URN = {urn:nbn:de:0030-drops-91964}, doi = {10.4230/LIPIcs.FSCD.2018.26}, annote = {Keywords: conditional term rewriting, innermost narrowing, regular tree grammar} } @InProceedings{parys:LIPIcs.FSCD.2018.27, author = {Parys, Pawel}, title = {{Homogeneity Without Loss of Generality}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {27:1--27:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.27}, URN = {urn:nbn:de:0030-drops-91972}, doi = {10.4230/LIPIcs.FSCD.2018.27}, annote = {Keywords: higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes} } @InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2018.28, author = {Schmidt-Schau{\ss}, Manfred and Sabel, David}, title = {{Nominal Unification with Atom and Context Variables}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {28:1--28:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.28}, URN = {urn:nbn:de:0030-drops-91983}, doi = {10.4230/LIPIcs.FSCD.2018.28}, annote = {Keywords: automated deduction, nominal unification, lambda calculus, functional programming} } @InProceedings{timany_et_al:LIPIcs.FSCD.2018.29, author = {Timany, Amin and Sozeau, Matthieu}, title = {{Cumulative Inductive Types In Coq}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {29:1--29:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.29}, URN = {urn:nbn:de:0030-drops-91991}, doi = {10.4230/LIPIcs.FSCD.2018.29}, annote = {Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity} } @InProceedings{winkler_et_al:LIPIcs.FSCD.2018.30, author = {Winkler, Sarah and Middeldorp, Aart}, title = {{Completion for Logically Constrained Rewriting}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {30:1--30:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.30}, URN = {urn:nbn:de:0030-drops-92001}, doi = {10.4230/LIPIcs.FSCD.2018.30}, annote = {Keywords: Constrained rewriting, completion, automation, theorem proving} } @InProceedings{kohl_et_al:LIPIcs.FSCD.2018.31, author = {Kohl, Christina and Middeldorp, Aart}, title = {{ProTeM: A Proof Term Manipulator}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {31:1--31:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.31}, URN = {urn:nbn:de:0030-drops-92013}, doi = {10.4230/LIPIcs.FSCD.2018.31}, annote = {Keywords: Proof terms, term rewriting, interactive tool} } @InProceedings{aoto_et_al:LIPIcs.FSCD.2018.32, author = {Aoto, Takahito and Hamana, Makoto and Hirokawa, Nao and Middeldorp, Aart and Nagele, Julian and Nishida, Naoki and Shintani, Kiraku and Zankl, Harald}, title = {{Confluence Competition 2018}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {32:1--32:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.32}, URN = {urn:nbn:de:0030-drops-92023}, doi = {10.4230/LIPIcs.FSCD.2018.32}, annote = {Keywords: Confluence, competition, rewrite systems} }