5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1-732, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@Proceedings{ariola:LIPIcs.FSCD.2020, title = {{LIPIcs, Volume 167, FSCD 2020, Complete Volume}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {1--732}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020}, URN = {urn:nbn:de:0030-drops-123219}, doi = {10.4230/LIPIcs.FSCD.2020}, annote = {Keywords: LIPIcs, Volume 167, FSCD 2020, Complete Volume} }
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{ariola:LIPIcs.FSCD.2020.0, author = {Ariola, Zena M.}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.0}, URN = {urn:nbn:de:0030-drops-123228}, doi = {10.4230/LIPIcs.FSCD.2020.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian. Solvability in a Probabilistic Setting (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{ronchidellarocca_et_al:LIPIcs.FSCD.2020.1, author = {Ronchi Della Rocca, Simona and Dal Lago, Ugo and Faggian, Claudia}, title = {{Solvability in a Probabilistic Setting}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {1:1--1:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.1}, URN = {urn:nbn:de:0030-drops-123237}, doi = {10.4230/LIPIcs.FSCD.2020.1}, annote = {Keywords: Probabilistic Computation, Lambda Calculus, Solvability, Intersection Types} }
Brigitte Pientka. A Modal Analysis of Metaprogramming, Revisited (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{pientka:LIPIcs.FSCD.2020.2, author = {Pientka, Brigitte}, title = {{A Modal Analysis of Metaprogramming, Revisited}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {2:1--2:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.2}, URN = {urn:nbn:de:0030-drops-123242}, doi = {10.4230/LIPIcs.FSCD.2020.2}, annote = {Keywords: Type systems, Metaprogramming, Modal Type System} }
Andrew M. Pitts. Quotients in Dependent Type Theory (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{pitts:LIPIcs.FSCD.2020.3, author = {Pitts, Andrew M.}, title = {{Quotients in Dependent Type Theory}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {3:1--3:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.3}, URN = {urn:nbn:de:0030-drops-123256}, doi = {10.4230/LIPIcs.FSCD.2020.3}, annote = {Keywords: dependent type theory, quotient, quotient inductive type, theorem-proving systems} }
René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada. Certifying the Weighted Path Order (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{thiemann_et_al:LIPIcs.FSCD.2020.4, author = {Thiemann, Ren\'{e} and Sch\"{o}pf, Jonas and Sternagel, Christian and Yamada, Akihisa}, title = {{Certifying the Weighted Path Order}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {4:1--4:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.4}, URN = {urn:nbn:de:0030-drops-123263}, doi = {10.4230/LIPIcs.FSCD.2020.4}, annote = {Keywords: certification, Isabelle/HOL, reduction order, termination analysis} }
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5, author = {Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa}, title = {{Efficient Full Higher-Order Unification}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.5}, URN = {urn:nbn:de:0030-drops-123271}, doi = {10.4230/LIPIcs.FSCD.2020.5}, annote = {Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures} }
Paul-André Melliès and Nicolas Rolland. Comprehension and Quotient Structures in the Language of 2-Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{mellies_et_al:LIPIcs.FSCD.2020.6, author = {Melli\`{e}s, Paul-Andr\'{e} and Rolland, Nicolas}, title = {{Comprehension and Quotient Structures in the Language of 2-Categories}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {6:1--6:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.6}, URN = {urn:nbn:de:0030-drops-123282}, doi = {10.4230/LIPIcs.FSCD.2020.6}, annote = {Keywords: Comprehension structures, quotient structures, comprehension structures with section, comprehension structures with image, 2-categories, formal adjunctions, path objects, categorical logic, inductive reasoning on algebras, coinductive reasoning on coalgebras} }
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{biernacki_et_al:LIPIcs.FSCD.2020.7, author = {Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr}, title = {{A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {7:1--7:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.7}, URN = {urn:nbn:de:0030-drops-123295}, doi = {10.4230/LIPIcs.FSCD.2020.7}, annote = {Keywords: algebraic effect, handler, behavioral equivalence, bisimilarity} }
Paul Brunet and David Pym. Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{brunet_et_al:LIPIcs.FSCD.2020.8, author = {Brunet, Paul and Pym, David}, title = {{Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.8}, URN = {urn:nbn:de:0030-drops-123308}, doi = {10.4230/LIPIcs.FSCD.2020.8}, annote = {Keywords: Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules} }
Andrej Dudenhefner. Undecidability of Semi-Unification on a Napkin. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{dudenhefner:LIPIcs.FSCD.2020.9, author = {Dudenhefner, Andrej}, title = {{Undecidability of Semi-Unification on a Napkin}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.9}, URN = {urn:nbn:de:0030-drops-123311}, doi = {10.4230/LIPIcs.FSCD.2020.9}, annote = {Keywords: undecidability, semi-unification, mechanization} }
Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional Bisimilarity for Reactive Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{hulsbusch_et_al:LIPIcs.FSCD.2020.10, author = {H\"{u}lsbusch, Mathias and K\"{o}nig, Barbara and K\"{u}pper, Sebastian and Stoltenow, Lara}, title = {{Conditional Bisimilarity for Reactive Systems}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {10:1--10:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.10}, URN = {urn:nbn:de:0030-drops-123322}, doi = {10.4230/LIPIcs.FSCD.2020.10}, annote = {Keywords: conditional bisimilarity, reactive systems, up-to context, graph transformation} }
Masaomi Yamaguchi and Takahito Aoto. A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{yamaguchi_et_al:LIPIcs.FSCD.2020.11, author = {Yamaguchi, Masaomi and Aoto, Takahito}, title = {{A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {11:1--11:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.11}, URN = {urn:nbn:de:0030-drops-123338}, doi = {10.4230/LIPIcs.FSCD.2020.11}, annote = {Keywords: uniqueness of normal forms w.r.t. conversion, shallow term rewriting systems, decision procedure} }
André Hirschowitz, Tom Hirschowitz, and Ambroise Lafont. Modules over Monads and Operational Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{hirschowitz_et_al:LIPIcs.FSCD.2020.12, author = {Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Lafont, Ambroise}, title = {{Modules over Monads and Operational Semantics}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {12:1--12:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.12}, URN = {urn:nbn:de:0030-drops-123341}, doi = {10.4230/LIPIcs.FSCD.2020.12}, annote = {Keywords: Operational semantics, Category theory} }
Frédéric Blanqui. Type Safety of Rewrite Rules in Dependent Types. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{blanqui:LIPIcs.FSCD.2020.13, author = {Blanqui, Fr\'{e}d\'{e}ric}, title = {{Type Safety of Rewrite Rules in Dependent Types}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {13:1--13:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.13}, URN = {urn:nbn:de:0030-drops-123353}, doi = {10.4230/LIPIcs.FSCD.2020.13}, annote = {Keywords: subject-reduction, rewriting, dependent types} }
Rose Bohrer and André Platzer. Refining Constructive Hybrid Games. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{bohrer_et_al:LIPIcs.FSCD.2020.14, author = {Bohrer, Rose and Platzer, Andr\'{e}}, title = {{Refining Constructive Hybrid Games}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {14:1--14:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.14}, URN = {urn:nbn:de:0030-drops-123369}, doi = {10.4230/LIPIcs.FSCD.2020.14}, annote = {Keywords: Hybrid Games, Constructive Logic, Refinement, Game Logic} }
Andrej Ivašković, Alan Mycroft, and Dominic Orchard. Data-Flow Analyses as Effects and Graded Monads. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{ivaskovic_et_al:LIPIcs.FSCD.2020.15, author = {Iva\v{s}kovi\'{c}, Andrej and Mycroft, Alan and Orchard, Dominic}, title = {{Data-Flow Analyses as Effects and Graded Monads}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {15:1--15:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.15}, URN = {urn:nbn:de:0030-drops-123376}, doi = {10.4230/LIPIcs.FSCD.2020.15}, annote = {Keywords: data-flow analysis, effect systems, graded monads, correctness} }
Zeinab Galal. A Profunctorial Scott Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{galal:LIPIcs.FSCD.2020.16, author = {Galal, Zeinab}, title = {{A Profunctorial Scott Semantics}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {16:1--16:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.16}, URN = {urn:nbn:de:0030-drops-123387}, doi = {10.4230/LIPIcs.FSCD.2020.16}, annote = {Keywords: Linear Logic, Scott Semantics, Profunctors} }
Guillaume Boisseau. String Diagrams for Optics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{boisseau:LIPIcs.FSCD.2020.17, author = {Boisseau, Guillaume}, title = {{String Diagrams for Optics}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {17:1--17:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.17}, URN = {urn:nbn:de:0030-drops-123399}, doi = {10.4230/LIPIcs.FSCD.2020.17}, annote = {Keywords: Optic, string diagram, lens, category theory, Yoneda lemma} }
Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski. A Reflection on Continuation-Composing Style. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{biernacki_et_al:LIPIcs.FSCD.2020.18, author = {Biernacki, Dariusz and Pyzik, Mateusz and Sieczkowski, Filip}, title = {{A Reflection on Continuation-Composing Style}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {18:1--18:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.18}, URN = {urn:nbn:de:0030-drops-123402}, doi = {10.4230/LIPIcs.FSCD.2020.18}, annote = {Keywords: delimited control, continuation-passing style, reflection, call-by-value lambda calculus, computational lambda calculus} }
Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada. A Probabilistic Higher-Order Fixpoint Logic. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{mitani_et_al:LIPIcs.FSCD.2020.19, author = {Mitani, Yo and Kobayashi, Naoki and Tsukada, Takeshi}, title = {{A Probabilistic Higher-Order Fixpoint Logic}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {19:1--19:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.19}, URN = {urn:nbn:de:0030-drops-123413}, doi = {10.4230/LIPIcs.FSCD.2020.19}, annote = {Keywords: Probabilistic logics, higher-order fixpoint logic, model checking} }
Rick Erkens and Maurice Laveaux. Adaptive Non-Linear Pattern Matching Automata. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{erkens_et_al:LIPIcs.FSCD.2020.20, author = {Erkens, Rick and Laveaux, Maurice}, title = {{Adaptive Non-Linear Pattern Matching Automata}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {20:1--20:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.20}, URN = {urn:nbn:de:0030-drops-123427}, doi = {10.4230/LIPIcs.FSCD.2020.20}, annote = {Keywords: Pattern matching, Term indexing, Tree automata} }
Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. On Average-Case Hardness of Higher-Order Model Checking. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{nakamura_et_al:LIPIcs.FSCD.2020.21, author = {Nakamura, Yoshiki and Asada, Kazuyuki and Kobayashi, Naoki and Sin'ya, Ryoma and Tsukada, Takeshi}, title = {{On Average-Case Hardness of Higher-Order Model Checking}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {21:1--21:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.21}, URN = {urn:nbn:de:0030-drops-123439}, doi = {10.4230/LIPIcs.FSCD.2020.21}, annote = {Keywords: Higher-order model checking, average-case complexity, intersection type system} }
Kazuyuki Asada and Naoki Kobayashi. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{asada_et_al:LIPIcs.FSCD.2020.22, author = {Asada, Kazuyuki and Kobayashi, Naoki}, title = {{Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {22:1--22:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.22}, URN = {urn:nbn:de:0030-drops-123440}, doi = {10.4230/LIPIcs.FSCD.2020.22}, annote = {Keywords: higher-order grammar, word language, tree language, complexity} }
Ambrus Kaposi and Jakob von Raumer. A Syntax for Mutual Inductive Families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2020.23, author = {Kaposi, Ambrus and von Raumer, Jakob}, title = {{A Syntax for Mutual Inductive Families}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {23:1--23:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.23}, URN = {urn:nbn:de:0030-drops-123451}, doi = {10.4230/LIPIcs.FSCD.2020.23}, annote = {Keywords: type theory, inductive types, mutual inductive types, W-types, Agda} }
Tim Lukas Diezel and Sergey Goncharov. Towards Constructive Hybrid Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{diezel_et_al:LIPIcs.FSCD.2020.24, author = {Diezel, Tim Lukas and Goncharov, Sergey}, title = {{Towards Constructive Hybrid Semantics}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.24}, URN = {urn:nbn:de:0030-drops-123466}, doi = {10.4230/LIPIcs.FSCD.2020.24}, annote = {Keywords: Hybrid semantics, Elgot iteration, Homotopy type theory, Agda} }
Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{xu:LIPIcs.FSCD.2020.25, author = {Xu, Chuangjie}, title = {{A Gentzen-Style Monadic Translation of G\"{o}del’s System T}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {25:1--25:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.25}, URN = {urn:nbn:de:0030-drops-123472}, doi = {10.4230/LIPIcs.FSCD.2020.25}, annote = {Keywords: monadic translation, G\"{o}del’s System T, logical relation, negative translation, majorizability, continuity, bar recursion, Agda} }
David M. Cerna and Temur Kutsia. Unital Anti-Unification: Type and Algorithms. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{cerna_et_al:LIPIcs.FSCD.2020.26, author = {Cerna, David M. and Kutsia, Temur}, title = {{Unital Anti-Unification: Type and Algorithms}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.26}, URN = {urn:nbn:de:0030-drops-123482}, doi = {10.4230/LIPIcs.FSCD.2020.26}, annote = {Keywords: Anti-unification, tree grammars, unital theories, collapse theories} }
Yu-Yang Lin and Nikos Tzevelekos. Symbolic Execution Game Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{lin_et_al:LIPIcs.FSCD.2020.27, author = {Lin, Yu-Yang and Tzevelekos, Nikos}, title = {{Symbolic Execution Game Semantics}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {27:1--27:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.27}, URN = {urn:nbn:de:0030-drops-123493}, doi = {10.4230/LIPIcs.FSCD.2020.27}, annote = {Keywords: game semantics, symbolic execution, higher-order open programs} }
Wilmer Ricciotti and James Cheney. Strongly Normalizing Higher-Order Relational Queries. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 28:1-28:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{ricciotti_et_al:LIPIcs.FSCD.2020.28, author = {Ricciotti, Wilmer and Cheney, James}, title = {{Strongly Normalizing Higher-Order Relational Queries}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {28:1--28:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.28}, URN = {urn:nbn:de:0030-drops-123506}, doi = {10.4230/LIPIcs.FSCD.2020.28}, annote = {Keywords: Strong normalization, ⊤⊤-lifting, Nested relational calculus, Language-integrated query} }
Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-Axiomatic Sequent Calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{deyoung_et_al:LIPIcs.FSCD.2020.29, author = {DeYoung, Henry and Pfenning, Frank and Pruiksma, Klaas}, title = {{Semi-Axiomatic Sequent Calculus}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {29:1--29:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.29}, URN = {urn:nbn:de:0030-drops-123515}, doi = {10.4230/LIPIcs.FSCD.2020.29}, annote = {Keywords: Sequent calculus, Curry-Howard isomorphism, shared memory concurrency} }
Besik Dundua, Temur Kutsia, Mircea Marin, and Cleopatra Pau. Constraint Solving over Multiple Similarity Relations. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{dundua_et_al:LIPIcs.FSCD.2020.30, author = {Dundua, Besik and Kutsia, Temur and Marin, Mircea and Pau, Cleopatra}, title = {{Constraint Solving over Multiple Similarity Relations}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.30}, URN = {urn:nbn:de:0030-drops-123522}, doi = {10.4230/LIPIcs.FSCD.2020.30}, annote = {Keywords: Fuzzy relations, similarity, constraint solving} }
Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{genestier:LIPIcs.FSCD.2020.31, author = {Genestier, Guillaume}, title = {{Encoding Agda Programs Using Rewriting}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.31}, URN = {urn:nbn:de:0030-drops-123530}, doi = {10.4230/LIPIcs.FSCD.2020.31}, annote = {Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion} }
Mario Alvarez-Picallo and C.-H. Luke Ong. The Difference λ-Calculus: A Language for Difference Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2020.32, author = {Alvarez-Picallo, Mario and Ong, C.-H. Luke}, title = {{The Difference \lambda-Calculus: A Language for Difference Categories}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {32:1--32:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.32}, URN = {urn:nbn:de:0030-drops-123549}, doi = {10.4230/LIPIcs.FSCD.2020.32}, annote = {Keywords: Cartesian difference categories, Cartesian differential categories, Change actions, Differential lambda-calculus, Difference lambda-calculus} }
Ankush Das and Frank Pfenning. Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{das_et_al:LIPIcs.FSCD.2020.33, author = {Das, Ankush and Pfenning, Frank}, title = {{Rast: Resource-Aware Session Types with Arithmetic Refinements}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {33:1--33:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.33}, URN = {urn:nbn:de:0030-drops-123558}, doi = {10.4230/LIPIcs.FSCD.2020.33}, annote = {Keywords: Session Types, Resource Analysis, Refinement Types} }
Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{cohen_et_al:LIPIcs.FSCD.2020.34, author = {Cohen, Cyril and Sakaguchi, Kazuhiko and Tassi, Enrico}, title = {{Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {34:1--34:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.34}, URN = {urn:nbn:de:0030-drops-123562}, doi = {10.4230/LIPIcs.FSCD.2020.34}, annote = {Keywords: Algebraic Hierarchy, Packed Classes, Coq, Elpi, Metaprogramming, \lambdaProlog} }
Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{hondet_et_al:LIPIcs.FSCD.2020.35, author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric}, title = {{The New Rewriting Engine of Dedukti}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {35:1--35:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.35}, URN = {urn:nbn:de:0030-drops-123577}, doi = {10.4230/LIPIcs.FSCD.2020.35}, annote = {Keywords: rewriting, higher-order pattern-matching, decision trees} }
Cynthia Kop. WANDA - a Higher Order Termination Tool (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{kop:LIPIcs.FSCD.2020.36, author = {Kop, Cynthia}, title = {{WANDA - a Higher Order Termination Tool}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {36:1--36:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.36}, URN = {urn:nbn:de:0030-drops-123587}, doi = {10.4230/LIPIcs.FSCD.2020.36}, annote = {Keywords: higher-order term rewriting, termination, automatic analysis, dependency pair framework, higher-order recursive path ordering} }
Claude Stolze and Luigi Liquori. A Type Checker for a Logical Framework with Union and Intersection Types (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 37:1-37:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{stolze_et_al:LIPIcs.FSCD.2020.37, author = {Stolze, Claude and Liquori, Luigi}, title = {{A Type Checker for a Logical Framework with Union and Intersection Types}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {37:1--37:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.37}, URN = {urn:nbn:de:0030-drops-123597}, doi = {10.4230/LIPIcs.FSCD.2020.37}, annote = {Keywords: Intersection types, Union types, Dependent types, Subtyping, Type checker, Refiner, \Delta-Framework} }
Feedback for Dagstuhl Publishing