3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Stéphanie Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Peter Selinger. Challenges in Quantum Programming Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Valeria Vignudelli. Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Sandra Alves and Sabine Broda. A Unifying Framework for Type Inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Nirina Andrianarivelo and Pierre Réty. Confluence of Prefix-Constrained Rewrite Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Term-Graph Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Gianluigi Bellin and Willem B. Heijltjes. Proof Nets for Bi-Intuitionistic Linear Logic. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Maciej Bendkowski and Pierre Lescanne. Counting Environments and Closures. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
David M. Cerna and Temur Kutsia. Higher-Order Equational Pattern Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Simon Forest and Samuel Mimram. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Thomas Genet. Completeness of Tree Automata Completion. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Amar Hadzihasanovic, Giovanni de Felice, and Kang Feng Ng. A Diagrammatic Axiomatisation of Fermionic Quantum Circuits. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Mirai Ikebuchi and Keisuke Nakano. On Repetitive Right Application of B-Terms. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. Index-Stratified Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Ambrus Kaposi and András Kovács. A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Jean-Simon Pacaud Lemay. Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Bassel Mannaa and Rasmus Ejlers Møgelberg. The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Max S. New and Daniel R. Licata. Call-by-Name Gradual Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Lê Thành Dung Nguyen. Unique perfect matchings and proof nets. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Naoki Nishida and Yuya Maeda. Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Pawel Parys. Homogeneity Without Loss of Generality. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Manfred Schmidt-Schauß and David Sabel. Nominal Unification with Atom and Context Variables. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Amin Timany and Matthieu Sozeau. Cumulative Inductive Types In Coq. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Sarah Winkler and Aart Middeldorp. Completion for Logically Constrained Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Christina Kohl and Aart Middeldorp. ProTeM: A Proof Term Manipulator (System Description). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 31:1-31:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl. Confluence Competition 2018. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 32:1-32:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }