@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing