LIPIcs, Volume 84
FSCD 2017, September 3-9, 2017, Oxford, UK
Editors: Dale Miller
Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3, author = {Pimentel, Elaine and Pereira, Luiz Carlos}, title = {{A Tour on Ecumenical Systems}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3}, URN = {urn:nbn:de:0030-drops-188003}, doi = {10.4230/LIPIcs.CALCO.2023.3}, annote = {Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Nikolai Kudasov. E-Unification for Second-Order Abstract Syntax. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{kudasov:LIPIcs.FSCD.2023.10, author = {Kudasov, Nikolai}, title = {{E-Unification for Second-Order Abstract Syntax}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {10:1--10:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10}, URN = {urn:nbn:de:0030-drops-179944}, doi = {10.4230/LIPIcs.FSCD.2023.10}, annote = {Keywords: E-unification, higher-order unification, second-order abstract syntax} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Dale Miller and Jui-Hsuan Wu. A Positive Perspective on Term Representation (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 3:1-3:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{miller_et_al:LIPIcs.CSL.2023.3, author = {Miller, Dale and Wu, Jui-Hsuan}, title = {{A Positive Perspective on Term Representation}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {3:1--3:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.3}, URN = {urn:nbn:de:0030-drops-174648}, doi = {10.4230/LIPIcs.CSL.2023.3}, annote = {Keywords: term representation, sharing, focused proof systems} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21, author = {D{\'\i}az-Caro, Alejandro and Dowek, Gilles}, title = {{Linear Lambda-Calculus is Linear}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21}, URN = {urn:nbn:de:0030-drops-163024}, doi = {10.4230/LIPIcs.FSCD.2022.21}, annote = {Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 10:1-10:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{manighetti_et_al:LIPIcs.TYPES.2020.10, author = {Manighetti, Matteo and Miller, Dale and Momigliano, Alberto}, title = {{Two Applications of Logic Programming to Coq}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {10:1--10:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-182-5}, ISSN = {1868-8969}, year = {2021}, volume = {188}, editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.10}, URN = {urn:nbn:de:0030-drops-138896}, doi = {10.4230/LIPIcs.TYPES.2020.10}, annote = {Keywords: Proof assistants, logic programming, Coq, \lambdaProlog, property-based testing} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 1:1-1:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{miller:LIPIcs.TYPES.2016.1, author = {Miller, Dale}, title = {{Mechanized Metatheory Revisited: An Extended Abstract}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {1:1--1:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.1}, URN = {urn:nbn:de:0030-drops-98603}, doi = {10.4230/LIPIcs.TYPES.2016.1}, annote = {Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Dale Miller. LIPIcs, Volume 84, FSCD'17, Complete Volume. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@Proceedings{miller:LIPIcs.FSCD.2017, title = {{LIPIcs, Volume 84, FSCD'17, Complete Volume}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017}, URN = {urn:nbn:de:0030-drops-79063}, doi = {10.4230/LIPIcs.FSCD.2017}, annote = {Keywords: Theory of Computation, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity, Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Programming Techniques, Software/Program Verification, Programming Languages, Deduction and Theorem Proving} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Dale Miller. Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 0:i-0:xiv, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{miller:LIPIcs.FSCD.2017.0, author = {Miller, Dale}, title = {{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {0:i--0:xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.0}, URN = {urn:nbn:de:0030-drops-77126}, doi = {10.4230/LIPIcs.FSCD.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Marco Gaboardi. Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{gaboardi:LIPIcs.FSCD.2017.1, author = {Gaboardi, Marco}, title = {{Type Systems for the Relational Verification of Higher Order Programs}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {1:1--1:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.1}, URN = {urn:nbn:de:0030-drops-77429}, doi = {10.4230/LIPIcs.FSCD.2017.1}, annote = {Keywords: Relational verification, refinement types, type and effect systems, complexity analysis} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Georg Moser. Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 2:1-2:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{moser:LIPIcs.FSCD.2017.2, author = {Moser, Georg}, title = {{Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {2:1--2:10}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.2}, URN = {urn:nbn:de:0030-drops-77438}, doi = {10.4230/LIPIcs.FSCD.2017.2}, annote = {Keywords: resource analysis, term rewriting, automation} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Alexandra Silva. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 3:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{silva:LIPIcs.FSCD.2017.3, author = {Silva, Alexandra}, title = {{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.3}, URN = {urn:nbn:de:0030-drops-77445}, doi = {10.4230/LIPIcs.FSCD.2017.3}, annote = {Keywords: Kleene algebras, Pomset languages, concurrency, NetKAT} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Christine Tasson. Quantitative Semantics for Probabilistic Programming (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 4:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{tasson:LIPIcs.FSCD.2017.4, author = {Tasson, Christine}, title = {{Quantitative Semantics for Probabilistic Programming}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {4:1--4:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.4}, URN = {urn:nbn:de:0030-drops-77456}, doi = {10.4230/LIPIcs.FSCD.2017.4}, annote = {Keywords: denotational semantics, probabilistic programming, programming language, probability} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2017.5, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu}, title = {{Displayed Categories}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.5}, URN = {urn:nbn:de:0030-drops-77220}, doi = {10.4230/LIPIcs.FSCD.2017.5}, annote = {Keywords: Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Yohji Akama. The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 6:1-6:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{akama:LIPIcs.FSCD.2017.6, author = {Akama, Yohji}, title = {{The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.6}, URN = {urn:nbn:de:0030-drops-77346}, doi = {10.4230/LIPIcs.FSCD.2017.6}, annote = {Keywords: reducibility method, restricted reducibility theorem, sum type, typedirected expansion, strong normalization} }
Feedback for Dagstuhl Publishing