1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Amal Ahmed. Compositional Compiler Verification for a Multi-Language World. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Ichiro Hasuo. Coalgebras and Higher-Order Computation: a GoI Approach. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Gérard Huet. Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Ofer Arieli and Arnon Avron. Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Martin Avanzini and Georg Moser. Complexity of Acyclic Term Graph Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Valentin Blot. Classical Extraction in Continuation Models. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Jon Haël Brenas, Rachid Echahed, and Martin Strecker. Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Fer-Jan de Vries. On Undefined and Meaningless in Lambda Definability. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Intersection Type Unification Problem. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Makoto Hamana. Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Stefan Kahrs and Connor Smith. Non-Omega-Overlapping TRSs are UN. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
James Laird. Weighted Relational Models for Mobility. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Olivier Laurent. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Tomer Libal and Dale Miller. Functions-as-Constructors Higher-Order Unification. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Naoki Nishida, Adrián Palacios, and Germán Vidal. Reversible Term Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Christian Sternagel and Thomas Sternagel. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Dmitriy Traytel. Formal Languages, Formally and Coinductively. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Takahito Aoto and Yoshihito Toyama. Ground Confluence Prover based on Rewriting Induction. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Stéphane Gimenez and David Obwaller. Interaction Automata and the ia2d Interpreter. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 35:1-35:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Franziska Rapp and Aart Middeldorp. Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@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-dev.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} }
Feedback for Dagstuhl Publishing