@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
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