@Proceedings{geuvers:LIPIcs.FSCD.2019, title = {{LIPIcs, Volume 131, FSCD'19, Complete Volume}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019}, URN = {urn:nbn:de:0030-drops-107734}, doi = {10.4230/LIPIcs.FSCD.2019}, annote = {Keywords: Theory of computation, Models of computation, Formal languages and automata theory, Logic, Semantics and reasoning} } @InProceedings{geuvers:LIPIcs.FSCD.2019.0, author = {Geuvers, Herman}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.0}, URN = {urn:nbn:de:0030-drops-105070}, doi = {10.4230/LIPIcs.FSCD.2019.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{accattoli:LIPIcs.FSCD.2019.1, author = {Accattoli, Beniamino}, title = {{A Fresh Look at the lambda-Calculus}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {1:1--1:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.1}, URN = {urn:nbn:de:0030-drops-105083}, doi = {10.4230/LIPIcs.FSCD.2019.1}, annote = {Keywords: lambda-calculus, sharing, abstract machines, type systems, rewriting} } @InProceedings{felty:LIPIcs.FSCD.2019.2, author = {Felty, Amy P.}, title = {{A Linear Logical Framework in Hybrid}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {2:1--2:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.2}, URN = {urn:nbn:de:0030-drops-105099}, doi = {10.4230/LIPIcs.FSCD.2019.2}, annote = {Keywords: Logical frameworks, proof assistants, linear logic} } @InProceedings{winkler:LIPIcs.FSCD.2019.3, author = {Winkler, Sarah}, title = {{Extending Maximal Completion}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.3}, URN = {urn:nbn:de:0030-drops-105102}, doi = {10.4230/LIPIcs.FSCD.2019.3}, annote = {Keywords: automated reasoning, completion, theorem proving} } @InProceedings{yang:LIPIcs.FSCD.2019.4, author = {Yang, Hongseok}, title = {{Some Semantic Issues in Probabilistic Programming Languages}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {4:1--4:6}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.4}, URN = {urn:nbn:de:0030-drops-105118}, doi = {10.4230/LIPIcs.FSCD.2019.4}, annote = {Keywords: Probabilistic Programming, Denotational Semantics, Non-differentiable Models, Bayesian Nonparametrics, Exchangeability} } @InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5, author = {Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels}, title = {{Bicategories in Univalent Foundations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5}, URN = {urn:nbn:de:0030-drops-105124}, doi = {10.4230/LIPIcs.FSCD.2019.5}, annote = {Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq} } @InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.6, author = {Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco}, title = {{Modular Specification of Monads Through Higher-Order Presentations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.6}, URN = {urn:nbn:de:0030-drops-105136}, doi = {10.4230/LIPIcs.FSCD.2019.6}, annote = {Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs} } @InProceedings{bendkowski:LIPIcs.FSCD.2019.7, author = {Bendkowski, Maciej}, title = {{Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {7:1--7:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.7}, URN = {urn:nbn:de:0030-drops-105144}, doi = {10.4230/LIPIcs.FSCD.2019.7}, annote = {Keywords: lambda calculus, explicit substitutions, complexity, combinatorics} } @InProceedings{biernacka_et_al:LIPIcs.FSCD.2019.8, author = {Biernacka, Ma{\l}gorzata and Charatonik, Witold}, title = {{Deriving an Abstract Machine for Strong Call by Need}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {8:1--8:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.8}, URN = {urn:nbn:de:0030-drops-105159}, doi = {10.4230/LIPIcs.FSCD.2019.8}, annote = {Keywords: abstract machines, reduction semantics} } @InProceedings{blanqui_et_al:LIPIcs.FSCD.2019.9, author = {Blanqui, Fr\'{e}d\'{e}ric and Genestier, Guillaume and Hermant, Olivier}, title = {{Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {9:1--9:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.9}, URN = {urn:nbn:de:0030-drops-105167}, doi = {10.4230/LIPIcs.FSCD.2019.9}, annote = {Keywords: termination, higher-order rewriting, dependent types, dependency pairs} } @InProceedings{cerna_et_al:LIPIcs.FSCD.2019.10, author = {Cerna, David M. and Kutsia, Temur}, title = {{A Generic Framework for Higher-Order Generalizations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {10:1--10:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.10}, URN = {urn:nbn:de:0030-drops-105175}, doi = {10.4230/LIPIcs.FSCD.2019.10}, annote = {Keywords: anti-unification, typed lambda calculus, least general generalization} } @InProceedings{coquand_et_al:LIPIcs.FSCD.2019.11, author = {Coquand, Thierry and Huber, Simon and Sattler, Christian}, title = {{Homotopy Canonicity for Cubical Type Theory}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {11:1--11:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11}, URN = {urn:nbn:de:0030-drops-105188}, doi = {10.4230/LIPIcs.FSCD.2019.11}, annote = {Keywords: cubical type theory, univalence, canonicity, sconing, Artin glueing} } @InProceedings{czajka_et_al:LIPIcs.FSCD.2019.12, author = {Czajka, {\L}ukasz and Kop, Cynthia}, title = {{Polymorphic Higher-Order Termination}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {12:1--12:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.12}, URN = {urn:nbn:de:0030-drops-105193}, doi = {10.4230/LIPIcs.FSCD.2019.12}, annote = {Keywords: termination, polymorphism, higher-order rewriting, permutative conversions} } @InProceedings{dallago_et_al:LIPIcs.FSCD.2019.13, author = {Dal Lago, Ugo and Leventis, Thomas}, title = {{On the Taylor Expansion of Probabilistic lambda-terms}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {13:1--13:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.13}, URN = {urn:nbn:de:0030-drops-105206}, doi = {10.4230/LIPIcs.FSCD.2019.13}, annote = {Keywords: Probabilistic Lambda-Calculi, Taylor Expansion, Linear Logic} } @InProceedings{diazcaro_et_al:LIPIcs.FSCD.2019.14, author = {D{\'\i}az-Caro, Alejandro and Dowek, Gilles}, title = {{Proof Normalisation in a Logic Identifying Isomorphic Propositions}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {14:1--14:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.14}, URN = {urn:nbn:de:0030-drops-105210}, doi = {10.4230/LIPIcs.FSCD.2019.14}, annote = {Keywords: Simply typed lambda calculus, Isomorphisms, Logic, Cut-elimination, Proof-reduction} } @InProceedings{ciaffaglione_et_al:LIPIcs.FSCD.2019.15, author = {Ciaffaglione, Alberto and Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan}, title = {{lambda!-calculus, Intersection Types, and Involutions}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.15}, URN = {urn:nbn:de:0030-drops-105228}, doi = {10.4230/LIPIcs.FSCD.2019.15}, annote = {Keywords: Affine Combinatory Algebra, Affine Lambda-calculus, Intersection Types, Geometry of Interaction} } @InProceedings{eberhart_et_al:LIPIcs.FSCD.2019.16, author = {Eberhart, Clovis and Hirschowitz, Tom and Laouar, Alexis}, title = {{Template Games, Simple Games, and Day Convolution}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {16:1--16:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.16}, URN = {urn:nbn:de:0030-drops-105237}, doi = {10.4230/LIPIcs.FSCD.2019.16}, annote = {Keywords: Game semantics, Day convolution, Categorical semantics} } @InProceedings{ehrhard:LIPIcs.FSCD.2019.17, author = {Ehrhard, Thomas}, title = {{Differentials and Distances in Probabilistic Coherence Spaces}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.17}, URN = {urn:nbn:de:0030-drops-105243}, doi = {10.4230/LIPIcs.FSCD.2019.17}, annote = {Keywords: Denotational semantics, probabilistic coherence spaces, differentials of programs} } @InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2019.18, author = {Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s and Uustalu, Tarmo}, title = {{Modal Embeddings and Calling Paradigms}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18}, URN = {urn:nbn:de:0030-drops-105256}, doi = {10.4230/LIPIcs.FSCD.2019.18}, annote = {Keywords: intuitionistic S4, call-by-name, call-by-value, comonadic lambda-calculus, standardization, indifference property} } @InProceedings{faggian:LIPIcs.FSCD.2019.19, author = {Faggian, Claudia}, title = {{Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {19:1--19:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.19}, URN = {urn:nbn:de:0030-drops-105263}, doi = {10.4230/LIPIcs.FSCD.2019.19}, annote = {Keywords: probabilistic rewriting, PARS, abstract rewriting systems, confluence, probabilistic lambda calculus} } @InProceedings{fukuda_et_al:LIPIcs.FSCD.2019.20, author = {Fukuda, Yosuke and Yoshimizu, Akira}, title = {{A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {20:1--20:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.20}, URN = {urn:nbn:de:0030-drops-105271}, doi = {10.4230/LIPIcs.FSCD.2019.20}, annote = {Keywords: linear logic, modal logic, Girard translation, Curry-Howard correspondence, geometry of interaction, staged computation} } @InProceedings{geser_et_al:LIPIcs.FSCD.2019.21, author = {Geser, Alfons and Hofbauer, Dieter and Waldmann, Johannes}, title = {{Sparse Tiling Through Overlap Closures for Termination of String Rewriting}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {21:1--21:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.21}, URN = {urn:nbn:de:0030-drops-105282}, doi = {10.4230/LIPIcs.FSCD.2019.21}, annote = {Keywords: relative termination, semantic labeling, locally testable language, overlap closure} } @InProceedings{heijltjes_et_al:LIPIcs.FSCD.2019.22, author = {Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz}, title = {{Proof Nets for First-Order Additive Linear Logic}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {22:1--22:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.22}, URN = {urn:nbn:de:0030-drops-105297}, doi = {10.4230/LIPIcs.FSCD.2019.22}, annote = {Keywords: linear logic, first-order logic, proof nets, Herbrand’s theorem} } @InProceedings{horne:LIPIcs.FSCD.2019.23, author = {Horne, Ross}, title = {{The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.23}, URN = {urn:nbn:de:0030-drops-105300}, doi = {10.4230/LIPIcs.FSCD.2019.23}, annote = {Keywords: calculus of structures, probabilistic choice, probabilistic refinement} } @InProceedings{ikebuchi:LIPIcs.FSCD.2019.24, author = {Ikebuchi, Mirai}, title = {{A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {24:1--24:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.24}, URN = {urn:nbn:de:0030-drops-105312}, doi = {10.4230/LIPIcs.FSCD.2019.24}, annote = {Keywords: Term rewriting systems, Equational logic, Homological algebra} } @InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25, author = {Kaposi, Ambrus and Huber, Simon and Sattler, Christian}, title = {{Gluing for Type Theory}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {25:1--25:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.25}, URN = {urn:nbn:de:0030-drops-105323}, doi = {10.4230/LIPIcs.FSCD.2019.25}, annote = {Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types} } @InProceedings{kasterovic_et_al:LIPIcs.FSCD.2019.26, author = {Ka\v{s}terovi\'{c}, Simona and Pagani, Michele}, title = {{The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.26}, URN = {urn:nbn:de:0030-drops-105338}, doi = {10.4230/LIPIcs.FSCD.2019.26}, annote = {Keywords: probabilistic lambda calculus, bisimulation, Howe’s technique, context equivalence, testing} } @InProceedings{larcheywendling_et_al:LIPIcs.FSCD.2019.27, author = {Larchey-Wendling, Dominique and Forster, Yannick}, title = {{Hilbert’s Tenth Problem in Coq}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {27:1--27:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.27}, URN = {urn:nbn:de:0030-drops-105342}, doi = {10.4230/LIPIcs.FSCD.2019.27}, annote = {Keywords: Hilbert’s tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory} } @InProceedings{liquori_et_al:LIPIcs.FSCD.2019.28, author = {Liquori, Luigi and Stolze, Claude}, title = {{The Delta-calculus: Syntax and Types}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {28:1--28:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.28}, URN = {urn:nbn:de:0030-drops-105354}, doi = {10.4230/LIPIcs.FSCD.2019.28}, annote = {Keywords: intersection types, lambda calculus \`{a} la Church and \`{a} la Curry, proof-functional logics} } @InProceedings{jacobedenaurois:LIPIcs.FSCD.2019.29, author = {Jacob\'{e} de Naurois, Paulin}, title = {{Pointers in Recursion: Exploring the Tropics}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.29}, URN = {urn:nbn:de:0030-drops-105360}, doi = {10.4230/LIPIcs.FSCD.2019.29}, annote = {Keywords: Implicit Complexity, Recursion Theory} } @InProceedings{pirog_et_al:LIPIcs.FSCD.2019.30, author = {Pir\'{o}g, Maciej and Polesiuk, Piotr and Sieczkowski, Filip}, title = {{Typed Equivalence of Effect Handlers and Delimited Control}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {30:1--30:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.30}, URN = {urn:nbn:de:0030-drops-105376}, doi = {10.4230/LIPIcs.FSCD.2019.30}, annote = {Keywords: type-and-effect systems, algebraic effects, delimited control, macro expressibility} } @InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31, author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel}, title = {{Cubical Syntax for Reflection-Free Extensional Equality}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {31:1--31:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31}, URN = {urn:nbn:de:0030-drops-105387}, doi = {10.4230/LIPIcs.FSCD.2019.31}, annote = {Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity} } @InProceedings{veltri_et_al:LIPIcs.FSCD.2019.32, author = {Veltri, Niccol\`{o} and van der Weide, Niels}, title = {{Guarded Recursion in Agda via Sized Types}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {32:1--32:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.32}, URN = {urn:nbn:de:0030-drops-105391}, doi = {10.4230/LIPIcs.FSCD.2019.32}, annote = {Keywords: guarded recursion, type theory, semantics, coinduction, sized types} } @InProceedings{vial:LIPIcs.FSCD.2019.33, author = {Vial, Pierre}, title = {{Sequence Types for Hereditary Permutators}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {33:1--33:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.33}, URN = {urn:nbn:de:0030-drops-105404}, doi = {10.4230/LIPIcs.FSCD.2019.33}, annote = {Keywords: hereditary permutators, B\"{o}hm trees, intersection types, coinduction, ridigity, sequence types, non-idempotent intersection} } @InProceedings{rubio_et_al:LIPIcs.FSCD.2019.34, author = {Rubio, Rub\'{e}n and Mart{\'\i}-Oliet, Narciso and Pita, Isabel and Verdejo, Alberto}, title = {{Model Checking Strategy-Controlled Rewriting Systems}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {34:1--34:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.34}, URN = {urn:nbn:de:0030-drops-105414}, doi = {10.4230/LIPIcs.FSCD.2019.34}, annote = {Keywords: Model checking, strategies, Maude, rewriting logic} }
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