@Proceedings{kesner_et_al:LIPIcs.FSCD.2016,
title = {{LIPIcs, Volume 52, FSCD'16, Complete Volume}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016},
URN = {urn:nbn:de:0030-drops-60595},
doi = {10.4230/LIPIcs.FSCD.2016},
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{kesner_et_al:LIPIcs.FSCD.2016.0,
author = {Kesner, Delia and Pientka, Brigitte},
title = {{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.0},
URN = {urn:nbn:de:0030-drops-59672},
doi = {10.4230/LIPIcs.FSCD.2016.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee}
}
@InProceedings{ahmed:LIPIcs.FSCD.2016.1,
author = {Ahmed, Amal},
title = {{Compositional Compiler Verification for a Multi-Language World}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.1},
URN = {urn:nbn:de:0030-drops-59680},
doi = {10.4230/LIPIcs.FSCD.2016.1},
annote = {Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages}
}
@InProceedings{hasuo:LIPIcs.FSCD.2016.2,
author = {Hasuo, Ichiro},
title = {{Coalgebras and Higher-Order Computation: a GoI Approach}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.2},
URN = {urn:nbn:de:0030-drops-59698},
doi = {10.4230/LIPIcs.FSCD.2016.2},
annote = {Keywords: functional programming, geometry of interaction, categorical semantics, coalgebra}
}
@InProceedings{huet:LIPIcs.FSCD.2016.3,
author = {Huet, G\'{e}rard},
title = {{Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {3:1--3:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.3},
URN = {urn:nbn:de:0030-drops-60020},
doi = {10.4230/LIPIcs.FSCD.2016.3},
annote = {Keywords: Foundations, Computation, Deduction, Programming, Proofs}
}
@InProceedings{nipkow:LIPIcs.FSCD.2016.4,
author = {Nipkow, Tobias},
title = {{Verified Analysis of Functional Data Structures}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {4:1--4:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.4},
URN = {urn:nbn:de:0030-drops-59701},
doi = {10.4230/LIPIcs.FSCD.2016.4},
annote = {Keywords: Program Verification, Algorithm Analysis, Functional Programming}
}
@InProceedings{akiyoshi_et_al:LIPIcs.FSCD.2016.5,
author = {Akiyoshi, Ryota and Terui, Kazushige},
title = {{Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {5:1--5:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5},
URN = {urn:nbn:de:0030-drops-59718},
doi = {10.4230/LIPIcs.FSCD.2016.5},
annote = {Keywords: Polymorphic Lambda Calculus, Strong Normalization, Computability Predicate, Infinitary Proof Theory}
}
@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2016.6,
author = {Altenkirch, Thorsten and Kaposi, Ambrus},
title = {{Normalisation by Evaluation for Dependent Types}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6},
URN = {urn:nbn:de:0030-drops-59727},
doi = {10.4230/LIPIcs.FSCD.2016.6},
annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}
@InProceedings{arieli_et_al:LIPIcs.FSCD.2016.7,
author = {Arieli, Ofer and Avron, Arnon},
title = {{Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.7},
URN = {urn:nbn:de:0030-drops-59731},
doi = {10.4230/LIPIcs.FSCD.2016.7},
annote = {Keywords: Paraconsistecy, Paracompleteness, 4-valued logics}
}
@InProceedings{arisaka:LIPIcs.FSCD.2016.8,
author = {Arisaka, Ryuta},
title = {{Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.8},
URN = {urn:nbn:de:0030-drops-59742},
doi = {10.4230/LIPIcs.FSCD.2016.8},
annote = {Keywords: cut-elimination, contraction-free, sequent calculus, proof theory, BI, logic combination}
}
@InProceedings{aristizabal_et_al:LIPIcs.FSCD.2016.9,
author = {Aristiz\'{a}bal, Andr\'{e}s and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr},
title = {{Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.9},
URN = {urn:nbn:de:0030-drops-59756},
doi = {10.4230/LIPIcs.FSCD.2016.9},
annote = {Keywords: delimited continuation, dynamic prompt generation, contextual equivalence, environmental bisimulation, up-to technique}
}
@InProceedings{avanzini_et_al:LIPIcs.FSCD.2016.10,
author = {Avanzini, Martin and Moser, Georg},
title = {{Complexity of Acyclic Term Graph Rewriting}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.10},
URN = {urn:nbn:de:0030-drops-59901},
doi = {10.4230/LIPIcs.FSCD.2016.10},
annote = {Keywords: Program Analysis, Graph Rewriting, Complexity Analysis}
}
@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2016.11,
author = {Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
title = {{Nominal Narrowing}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.11},
URN = {urn:nbn:de:0030-drops-59832},
doi = {10.4230/LIPIcs.FSCD.2016.11},
annote = {Keywords: Nominal Rewriting, Nominal Unification, Matching, Narrowing, Equational Theories}
}
@InProceedings{benke_et_al:LIPIcs.FSCD.2016.12,
author = {Benke, Marcin and Schubert, Aleksy and Walukiewicz-Chrzaszcz, Daria},
title = {{Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {12:1--12:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.12},
URN = {urn:nbn:de:0030-drops-59765},
doi = {10.4230/LIPIcs.FSCD.2016.12},
annote = {Keywords: ML, program synthesis}
}
@InProceedings{blot:LIPIcs.FSCD.2016.13,
author = {Blot, Valentin},
title = {{Classical Extraction in Continuation Models}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.13},
URN = {urn:nbn:de:0030-drops-59913},
doi = {10.4230/LIPIcs.FSCD.2016.13},
annote = {Keywords: Extraction, Classical Logic, Control Operators, Game Semantics}
}
@InProceedings{brenas_et_al:LIPIcs.FSCD.2016.14,
author = {Brenas, Jon Ha\"{e}l and Echahed, Rachid and Strecker, Martin},
title = {{Proving Correctness of Logically Decorated Graph Rewriting Systems}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {14:1--14:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.14},
URN = {urn:nbn:de:0030-drops-59778},
doi = {10.4230/LIPIcs.FSCD.2016.14},
annote = {Keywords: Graph Rewriting, Hoare Logic,Combinatory PDL, Rewrite Strategies, Program Verification}
}
@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15,
author = {Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico},
title = {{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15},
URN = {urn:nbn:de:0030-drops-59924},
doi = {10.4230/LIPIcs.FSCD.2016.15},
annote = {Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule}
}
@InProceedings{chaudhuri_et_al:LIPIcs.FSCD.2016.16,
author = {Chaudhuri, Kaustuv and Marin, Sonia and Stra{\ss}burger, Lutz},
title = {{Modular Focused Proof Systems for Intuitionistic Modal Logics}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.16},
URN = {urn:nbn:de:0030-drops-59947},
doi = {10.4230/LIPIcs.FSCD.2016.16},
annote = {Keywords: intuitionistic modal logic, focusing, proof search, cut elimination, nested sequents}
}
@InProceedings{coquand_et_al:LIPIcs.FSCD.2016.17,
author = {Coquand, Thierry and Mannaa, Bassel},
title = {{The Independence of Markov’s Principle in Type Theory}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.17},
URN = {urn:nbn:de:0030-drops-59939},
doi = {10.4230/LIPIcs.FSCD.2016.17},
annote = {Keywords: Forcing, Dependent type theory, Markov's Principle, Cantor Space}
}
@InProceedings{devries:LIPIcs.FSCD.2016.18,
author = {de Vries, Fer-Jan},
title = {{On Undefined and Meaningless in Lambda Definability}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {18:1--18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.18},
URN = {urn:nbn:de:0030-drops-59785},
doi = {10.4230/LIPIcs.FSCD.2016.18},
annote = {Keywords: lambda calculus, lambda definability, partial recursive function, undefined term, meaningless term}
}
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2016.19,
author = {Dudenhefner, Andrej and Martens, Moritz and Rehof, Jakob},
title = {{The Intersection Type Unification Problem}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {19:1--19:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.19},
URN = {urn:nbn:de:0030-drops-59955},
doi = {10.4230/LIPIcs.FSCD.2016.19},
annote = {Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity}
}
@InProceedings{guerrieri_et_al:LIPIcs.FSCD.2016.20,
author = {Guerrieri, Giulio and Pellissier, Luc and Tortora de Falco, Lorenzo},
title = {{Computing Connected Proof(-Structure)s From Their Taylor Expansion}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.20},
URN = {urn:nbn:de:0030-drops-60031},
doi = {10.4230/LIPIcs.FSCD.2016.20},
annote = {Keywords: proof-nets, (differential) linear logic, relational model, Taylor expansion}
}
@InProceedings{hamana:LIPIcs.FSCD.2016.21,
author = {Hamana, Makoto},
title = {{Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.21},
URN = {urn:nbn:de:0030-drops-59792},
doi = {10.4230/LIPIcs.FSCD.2016.21},
annote = {Keywords: cyclic data structures, traced cartesian category, fixed point, functional programming, fold}
}
@InProceedings{kahrs_et_al:LIPIcs.FSCD.2016.22,
author = {Kahrs, Stefan and Smith, Connor},
title = {{Non-Omega-Overlapping TRSs are UN}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.22},
URN = {urn:nbn:de:0030-drops-59968},
doi = {10.4230/LIPIcs.FSCD.2016.22},
annote = {Keywords: consistency, omega-substitutions, uniqueness of normal forms}
}
@InProceedings{kop_et_al:LIPIcs.FSCD.2016.23,
author = {Kop, Cynthia and Grue Simonsen, Jakob},
title = {{Complexity Hierarchies and Higher-Order Cons-Free Rewriting}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23},
URN = {urn:nbn:de:0030-drops-59972},
doi = {10.4230/LIPIcs.FSCD.2016.23},
annote = {Keywords: higher-order term rewriting, implicit complexity, cons-freeness, ETIME hierarchy}
}
@InProceedings{laird:LIPIcs.FSCD.2016.24,
author = {Laird, James},
title = {{Weighted Relational Models for Mobility}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {24:1--24:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.24},
URN = {urn:nbn:de:0030-drops-59982},
doi = {10.4230/LIPIcs.FSCD.2016.24},
annote = {Keywords: Concurrency, Mobility, Denotational Semantics}
}
@InProceedings{laurent:LIPIcs.FSCD.2016.25,
author = {Laurent, Olivier},
title = {{Focusing in Orthologic}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {25:1--25:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.25},
URN = {urn:nbn:de:0030-drops-59805},
doi = {10.4230/LIPIcs.FSCD.2016.25},
annote = {Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination}
}
@InProceedings{libal_et_al:LIPIcs.FSCD.2016.26,
author = {Libal, Tomer and Miller, Dale},
title = {{Functions-as-Constructors Higher-Order Unification}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {26:1--26:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.26},
URN = {urn:nbn:de:0030-drops-59810},
doi = {10.4230/LIPIcs.FSCD.2016.26},
annote = {Keywords: higher-order unification, pattern unification}
}
@InProceedings{malbos_et_al:LIPIcs.FSCD.2016.27,
author = {Malbos, Philippe and Mimram, Samuel},
title = {{Homological Computations for Term Rewriting Systems}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {27:1--27:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.27},
URN = {urn:nbn:de:0030-drops-59821},
doi = {10.4230/LIPIcs.FSCD.2016.27},
annote = {Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation}
}
@InProceedings{nishida_et_al:LIPIcs.FSCD.2016.28,
author = {Nishida, Naoki and Palacios, Adri\'{a}n and Vidal, Germ\'{a}n},
title = {{Reversible Term Rewriting}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.28},
URN = {urn:nbn:de:0030-drops-59841},
doi = {10.4230/LIPIcs.FSCD.2016.28},
annote = {Keywords: term rewriting, reversible computation, program transformation}
}
@InProceedings{sternagel_et_al:LIPIcs.FSCD.2016.29,
author = {Sternagel, Christian and Sternagel, Thomas},
title = {{Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.29},
URN = {urn:nbn:de:0030-drops-59996},
doi = {10.4230/LIPIcs.FSCD.2016.29},
annote = {Keywords: certification, conditional term rewriting, confluence, infeasible critical pairs, non-reachability}
}
@InProceedings{timany_et_al:LIPIcs.FSCD.2016.30,
author = {Timany, Amin and Jacobs, Bart},
title = {{Category Theory in Coq 8.5}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.30},
URN = {urn:nbn:de:0030-drops-60003},
doi = {10.4230/LIPIcs.FSCD.2016.30},
annote = {Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory}
}
@InProceedings{traytel:LIPIcs.FSCD.2016.31,
author = {Traytel, Dmitriy},
title = {{Formal Languages, Formally and Coinductively}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {31:1--31:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.31},
URN = {urn:nbn:de:0030-drops-59853},
doi = {10.4230/LIPIcs.FSCD.2016.31},
annote = {Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL}
}
@InProceedings{vanoostrom_et_al:LIPIcs.FSCD.2016.32,
author = {van Oostrom, Vincent and Toyama, Yoshihito},
title = {{Normalisation by Random Descent}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.32},
URN = {urn:nbn:de:0030-drops-59862},
doi = {10.4230/LIPIcs.FSCD.2016.32},
annote = {Keywords: strategy, hyper-normalisation, commutation, random descent}
}
@InProceedings{aoto_et_al:LIPIcs.FSCD.2016.33,
author = {Aoto, Takahito and Toyama, Yoshihito},
title = {{Ground Confluence Prover based on Rewriting Induction}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {33:1--33:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.33},
URN = {urn:nbn:de:0030-drops-59873},
doi = {10.4230/LIPIcs.FSCD.2016.33},
annote = {Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems}
}
@InProceedings{bar_et_al:LIPIcs.FSCD.2016.34,
author = {Bar, Krzysztof and Kissinger, Aleks and Vicary, Jamie},
title = {{Globular: An Online Proof Assistant for Higher-Dimensional Rewriting}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {34:1--34:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.34},
URN = {urn:nbn:de:0030-drops-59880},
doi = {10.4230/LIPIcs.FSCD.2016.34},
annote = {Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving}
}
@InProceedings{gimenez_et_al:LIPIcs.FSCD.2016.35,
author = {Gimenez, St\'{e}phane and Obwaller, David},
title = {{Interaction Automata and the ia2d Interpreter}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {35:1--35:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.35},
URN = {urn:nbn:de:0030-drops-59896},
doi = {10.4230/LIPIcs.FSCD.2016.35},
annote = {Keywords: Interaction nets, computation models, parallel computation, functional programming}
}
@InProceedings{rapp_et_al:LIPIcs.FSCD.2016.36,
author = {Rapp, Franziska and Middeldorp, Aart},
title = {{Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {36:1--36:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Kesner, Delia and Pientka, Brigitte},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.36},
URN = {urn:nbn:de:0030-drops-60018},
doi = {10.4230/LIPIcs.FSCD.2016.36},
annote = {Keywords: first-order theory, ground rewrite systems, automation, synthesis}
}
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