2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@Proceedings{miller:LIPIcs.FSCD.2017, title = {{LIPIcs, Volume 84, FSCD'17, Complete Volume}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017}, URN = {urn:nbn:de:0030-drops-79063}, doi = {10.4230/LIPIcs.FSCD.2017}, annote = {Keywords: Theory of Computation, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity, Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Programming Techniques, Software/Program Verification, Programming Languages, Deduction and Theorem Proving} }
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{miller:LIPIcs.FSCD.2017.0, author = {Miller, Dale}, title = {{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {0:i--0:xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.0}, URN = {urn:nbn:de:0030-drops-77126}, doi = {10.4230/LIPIcs.FSCD.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers} }
Marco Gaboardi. Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{gaboardi:LIPIcs.FSCD.2017.1, author = {Gaboardi, Marco}, title = {{Type Systems for the Relational Verification of Higher Order Programs}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {1:1--1:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.1}, URN = {urn:nbn:de:0030-drops-77429}, doi = {10.4230/LIPIcs.FSCD.2017.1}, annote = {Keywords: Relational verification, refinement types, type and effect systems, complexity analysis} }
Georg Moser. Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{moser:LIPIcs.FSCD.2017.2, author = {Moser, Georg}, title = {{Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {2:1--2:10}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.2}, URN = {urn:nbn:de:0030-drops-77438}, doi = {10.4230/LIPIcs.FSCD.2017.2}, annote = {Keywords: resource analysis, term rewriting, automation} }
Alexandra Silva. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{silva:LIPIcs.FSCD.2017.3, author = {Silva, Alexandra}, title = {{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.3}, URN = {urn:nbn:de:0030-drops-77445}, doi = {10.4230/LIPIcs.FSCD.2017.3}, annote = {Keywords: Kleene algebras, Pomset languages, concurrency, NetKAT} }
Christine Tasson. Quantitative Semantics for Probabilistic Programming (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{tasson:LIPIcs.FSCD.2017.4, author = {Tasson, Christine}, title = {{Quantitative Semantics for Probabilistic Programming}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {4:1--4:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.4}, URN = {urn:nbn:de:0030-drops-77456}, doi = {10.4230/LIPIcs.FSCD.2017.4}, annote = {Keywords: denotational semantics, probabilistic programming, programming language, probability} }
Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2017.5, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu}, title = {{Displayed Categories}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.5}, URN = {urn:nbn:de:0030-drops-77220}, doi = {10.4230/LIPIcs.FSCD.2017.5}, annote = {Keywords: Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics} }
Yohji Akama. The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{akama:LIPIcs.FSCD.2017.6, author = {Akama, Yohji}, title = {{The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.6}, URN = {urn:nbn:de:0030-drops-77346}, doi = {10.4230/LIPIcs.FSCD.2017.6}, annote = {Keywords: reducibility method, restricted reducibility theorem, sum type, typedirected expansion, strong normalization} }
Takahito Aoto, Yoshihito Toyama, and Yuta Kimura. Improving Rewriting Induction Approach for Proving Ground Confluence. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{aoto_et_al:LIPIcs.FSCD.2017.7, author = {Aoto, Takahito and Toyama, Yoshihito and Kimura, Yuta}, title = {{Improving Rewriting Induction Approach for Proving Ground Confluence}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {7:1--7:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.7}, URN = {urn:nbn:de:0030-drops-77310}, doi = {10.4230/LIPIcs.FSCD.2017.7}, annote = {Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems} }
Patrick Bahr. Böhm Reduction in Infinitary Term Graph Rewriting Systems. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{bahr:LIPIcs.FSCD.2017.8, author = {Bahr, Patrick}, title = {{B\"{o}hm Reduction in Infinitary Term Graph Rewriting Systems}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {8:1--8:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.8}, URN = {urn:nbn:de:0030-drops-77275}, doi = {10.4230/LIPIcs.FSCD.2017.8}, annote = {Keywords: infinitary rewriting, term graphs, B\"{o}hm trees} }
Pablo Barenbaum and Eduardo Bonelli. Optimality and the Linear Substitution Calculus. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{barenbaum_et_al:LIPIcs.FSCD.2017.9, author = {Barenbaum, Pablo and Bonelli, Eduardo}, title = {{Optimality and the Linear Substitution Calculus}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.9}, URN = {urn:nbn:de:0030-drops-77307}, doi = {10.4230/LIPIcs.FSCD.2017.9}, annote = {Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction} }
Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska. Generalized Refocusing: From Hybrid Strategies to Abstract Machines. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{biernacka_et_al:LIPIcs.FSCD.2017.10, author = {Biernacka, Malgorzata and Charatonik, Witold and Zielinska, Klara}, title = {{Generalized Refocusing: From Hybrid Strategies to Abstract Machines}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {10:1--10:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.10}, URN = {urn:nbn:de:0030-drops-77188}, doi = {10.4230/LIPIcs.FSCD.2017.10}, annote = {Keywords: reduction semantics, abstract machines, formal verification, Coq} }
Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{blanchette_et_al:LIPIcs.FSCD.2017.11, author = {Blanchette, Jasmin Christian and Fleury, Mathias and Traytel, Dmitriy}, title = {{Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.11}, URN = {urn:nbn:de:0030-drops-77155}, doi = {10.4230/LIPIcs.FSCD.2017.11}, annote = {Keywords: Multisets, ordinals, proof assistants} }
Simon Castellan, Pierre Clairambault, and Glynn Winskel. Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{castellan_et_al:LIPIcs.FSCD.2017.12, author = {Castellan, Simon and Clairambault, Pierre and Winskel, Glynn}, title = {{Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.12}, URN = {urn:nbn:de:0030-drops-77219}, doi = {10.4230/LIPIcs.FSCD.2017.12}, annote = {Keywords: Game semantics, parallel-or, concurrent games, event structures, full abstraction} }
J. Robin B. Cockett and Jean-Simon Lemay. There Is Only One Notion of Differentiation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{cockett_et_al:LIPIcs.FSCD.2017.13, author = {Cockett, J. Robin B. and Lemay, Jean-Simon}, title = {{There Is Only One Notion of Differentiation}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {13:1--13:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.13}, URN = {urn:nbn:de:0030-drops-77166}, doi = {10.4230/LIPIcs.FSCD.2017.13}, annote = {Keywords: Differential Categories, Linear Logic, Coalgebra Modalities, Bialgebra Modalities} }
Lukasz Czajka. Confluence of an Extension of Combinatory Logic by Boolean Constants. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{czajka:LIPIcs.FSCD.2017.14, author = {Czajka, Lukasz}, title = {{Confluence of an Extension of Combinatory Logic by Boolean Constants}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {14:1--14:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.14}, URN = {urn:nbn:de:0030-drops-77368}, doi = {10.4230/LIPIcs.FSCD.2017.14}, annote = {Keywords: combinatory logic, conditional linearization, unique normal form property, confluence} }
Andrej Dudenhefner and Jakob Rehof. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2017.15, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{The Complexity of Principal Inhabitation}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {15:1--15:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.15}, URN = {urn:nbn:de:0030-drops-77359}, doi = {10.4230/LIPIcs.FSCD.2017.15}, annote = {Keywords: Lambda Calculus, Type Theory, Simple Types, Inhabitation, Principal Type, Complexity} }
Marcelo Fiore and Philip Saville. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{fiore_et_al:LIPIcs.FSCD.2017.16, author = {Fiore, Marcelo and Saville, Philip}, title = {{List Objects with Algebraic Structure}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {16:1--16:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.16}, URN = {urn:nbn:de:0030-drops-77262}, doi = {10.4230/LIPIcs.FSCD.2017.16}, annote = {Keywords: list object, free monoid, strong monad, (cartesian, linear, and second-order) algebraic theory, near semiring, Haskell Monad type class, opetope} }
Stefano Guerrini and Marco Solieri. Is the Optimal Implementation Inefficient? Elementarily Not. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{guerrini_et_al:LIPIcs.FSCD.2017.17, author = {Guerrini, Stefano and Solieri, Marco}, title = {{Is the Optimal Implementation Inefficient? Elementarily Not}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {17:1--17:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.17}, URN = {urn:nbn:de:0030-drops-77337}, doi = {10.4230/LIPIcs.FSCD.2017.17}, annote = {Keywords: optimality, sharing graphs, lambda-calculus, complexity, linear logic, proof nets} }
Daniel Hillerström, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. Continuation Passing Style for Effect Handlers. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{hillerstrom_et_al:LIPIcs.FSCD.2017.18, author = {Hillerstr\"{o}m, Daniel and Lindley, Sam and Atkey, Robert and Sivaramakrishnan, K. C.}, title = {{Continuation Passing Style for Effect Handlers}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {18:1--18:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.18}, URN = {urn:nbn:de:0030-drops-77394}, doi = {10.4230/LIPIcs.FSCD.2017.18}, annote = {Keywords: effect handlers, delimited control, continuation passing style} }
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Infinite Runs in Abstract Completion. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{hirokawa_et_al:LIPIcs.FSCD.2017.19, author = {Hirokawa, Nao and Middeldorp, Aart and Sternagel, Christian and Winkler, Sarah}, title = {{Infinite Runs in Abstract Completion}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {19:1--19:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.19}, URN = {urn:nbn:de:0030-drops-77252}, doi = {10.4230/LIPIcs.FSCD.2017.19}, annote = {Keywords: term rewriting, abstract completion, ordered completion, canonicity, Isabelle/HOL} }
Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé's Longstanding Conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{intrigila_et_al:LIPIcs.FSCD.2017.20, author = {Intrigila, Benedetto and Manzonetto, Giulio and Polonsky, Andrew}, title = {{Refutation of Sall\'{e}'s Longstanding Conjecture}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20}, URN = {urn:nbn:de:0030-drops-77236}, doi = {10.4230/LIPIcs.FSCD.2017.20}, annote = {Keywords: lambda calculus, observational equivalence, B\"{o}hm trees, omega-rule} }
Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kaiser_et_al:LIPIcs.FSCD.2017.21, author = {Kaiser, Jonas and Pientka, Brigitte and Smolka, Gert}, title = {{Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {21:1--21:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.21}, URN = {urn:nbn:de:0030-drops-77248}, doi = {10.4230/LIPIcs.FSCD.2017.21}, annote = {Keywords: Pure Type Systems, System F, de Bruijn Syntax, Higher-Order Abstract Syntax, Contextual Reasoning} }
Max Kanovich, Stepan Kuznetsov, Glyn Morrill, and Andre Scedrov. A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kanovich_et_al:LIPIcs.FSCD.2017.22, author = {Kanovich, Max and Kuznetsov, Stepan and Morrill, Glyn and Scedrov, Andre}, title = {{A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {22:1--22:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.22}, URN = {urn:nbn:de:0030-drops-77387}, doi = {10.4230/LIPIcs.FSCD.2017.22}, annote = {Keywords: Lambek calculus, proof nets, Lambek calculus with brackets, categorial grammar, polynomial algorithm} }
Akitoshi Kawamura and Florian Steinberg. Polynomial Running Times for Polynomial-Time Oracle Machines. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kawamura_et_al:LIPIcs.FSCD.2017.23, author = {Kawamura, Akitoshi and Steinberg, Florian}, title = {{Polynomial Running Times for Polynomial-Time Oracle Machines}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {23:1--23:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.23}, URN = {urn:nbn:de:0030-drops-77370}, doi = {10.4230/LIPIcs.FSCD.2017.23}, annote = {Keywords: second-order complexity, oracle Turing machine, computable analysis, second-order polynomial, computational complexity of partial functionals} }
Delia Kesner and Pierre Vial. Types as Resources for Classical Natural Deduction. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2017.24, author = {Kesner, Delia and Vial, Pierre}, title = {{Types as Resources for Classical Natural Deduction}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {24:1--24:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.24}, URN = {urn:nbn:de:0030-drops-77135}, doi = {10.4230/LIPIcs.FSCD.2017.24}, annote = {Keywords: lambda-mu-calculus, classical logic, intersection types, normalization} }
Daniel R. Licata, Michael Shulman, and Mitchell Riley. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{licata_et_al:LIPIcs.FSCD.2017.25, author = {Licata, Daniel R. and Shulman, Michael and Riley, Mitchell}, title = {{A Fibrational Framework for Substructural and Modal Logics}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {25:1--25:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.25}, URN = {urn:nbn:de:0030-drops-77400}, doi = {10.4230/LIPIcs.FSCD.2017.25}, annote = {Keywords: type theory, modal logic, substructural logic, homotopy type theory} }
Benjamin Lichtman and Jan Hoffmann. Arrays and References in Resource Aware ML. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{lichtman_et_al:LIPIcs.FSCD.2017.26, author = {Lichtman, Benjamin and Hoffmann, Jan}, title = {{Arrays and References in Resource Aware ML}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.26}, URN = {urn:nbn:de:0030-drops-77282}, doi = {10.4230/LIPIcs.FSCD.2017.26}, annote = {Keywords: Resource Analysis, Functional Programming, Static Analysis, OCaml, Amortized Analysis} }
Tadeusz Litak, Miriam Polzer, and Ulrich Rabenstein. Negative Translations and Normal Modality. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{litak_et_al:LIPIcs.FSCD.2017.27, author = {Litak, Tadeusz and Polzer, Miriam and Rabenstein, Ulrich}, title = {{Negative Translations and Normal Modality}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {27:1--27:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.27}, URN = {urn:nbn:de:0030-drops-77412}, doi = {10.4230/LIPIcs.FSCD.2017.27}, annote = {Keywords: negative translations, intuitionistic modal logic, normal modality, double negation} }
Ian Orton and Andrew M. Pitts. Models of Type Theory Based on Moore Paths. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{orton_et_al:LIPIcs.FSCD.2017.28, author = {Orton, Ian and Pitts, Andrew M.}, title = {{Models of Type Theory Based on Moore Paths}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {28:1--28:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.28}, URN = {urn:nbn:de:0030-drops-77149}, doi = {10.4230/LIPIcs.FSCD.2017.28}, annote = {Keywords: dependent type theory, homotopy theory, Moore path, topos} }
Paolo Pistone. On Dinaturality, Typability and beta-eta-Stable Models. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{pistone:LIPIcs.FSCD.2017.29, author = {Pistone, Paolo}, title = {{On Dinaturality, Typability and beta-eta-Stable Models}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {29:1--29:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.29}, URN = {urn:nbn:de:0030-drops-77291}, doi = {10.4230/LIPIcs.FSCD.2017.29}, annote = {Keywords: Dinaturality, simply-typed lambda-calculus, beta-eta-stable semantics, completeness} }
Pierre Pradic and Colin Riba. A Curry-Howard Approach to Church's Synthesis. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{pradic_et_al:LIPIcs.FSCD.2017.30, author = {Pradic, Pierre and Riba, Colin}, title = {{A Curry-Howard Approach to Church's Synthesis}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {30:1--30:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.30}, URN = {urn:nbn:de:0030-drops-77198}, doi = {10.4230/LIPIcs.FSCD.2017.30}, annote = {Keywords: Intuitionistic Arithmetic, Realizability, Monadic Second-Order Logic on Infinite Words} }
Lutz Straßburger. Combinatorial Flows and Their Normalisation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{straburger:LIPIcs.FSCD.2017.31, author = {Stra{\ss}burger, Lutz}, title = {{Combinatorial Flows and Their Normalisation}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.31}, URN = {urn:nbn:de:0030-drops-77204}, doi = {10.4230/LIPIcs.FSCD.2017.31}, annote = {Keywords: proof equivalence, cut elimination, substitution, deep inference} }
Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada. Streett Automata Model Checking of Higher-Order Recursion Schemes. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{suzuki_et_al:LIPIcs.FSCD.2017.32, author = {Suzuki, Ryota and Fujima, Koichi and Kobayashi, Naoki and Tsukada, Takeshi}, title = {{Streett Automata Model Checking of Higher-Order Recursion Schemes}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {32:1--32:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.32}, URN = {urn:nbn:de:0030-drops-77325}, doi = {10.4230/LIPIcs.FSCD.2017.32}, annote = {Keywords: Higher-order model checking, higher-order recursion schemes, Streett automata} }
Noam Zeilberger. A Sequent Calculus for a Semi-Associative Law. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{zeilberger:LIPIcs.FSCD.2017.33, author = {Zeilberger, Noam}, title = {{A Sequent Calculus for a Semi-Associative Law}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.33}, URN = {urn:nbn:de:0030-drops-77179}, doi = {10.4230/LIPIcs.FSCD.2017.33}, annote = {Keywords: proof theory, combinatorics, coherence theorem, substructural logic, associativity} }
Feedback for Dagstuhl Publishing