LIPIcs, Volume 131
FSCD 2019, June 24-30, 2019, Dortmund, Germany
Editors: Herman Geuvers
LIPIcs, Volume 97
TYPES 2016, May 23-26, 2016, Novi Sad, Serbia
Editors: Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Herman Geuvers and Tonny Hurkens. Classical Natural Deduction from Truth Tables. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2022.2, author = {Geuvers, Herman and Hurkens, Tonny}, title = {{Classical Natural Deduction from Truth Tables}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {2:1--2:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.2}, URN = {urn:nbn:de:0030-drops-184450}, doi = {10.4230/LIPIcs.TYPES.2022.2}, annote = {Keywords: Natural deduction, classical proposition logic, multiple conclusion natural deduction, proof terms, formulas-as-types, proof normalization, subformula property, Curry-Howard isomorphism} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{krebbers:LIPIcs.ITP.2023.2, author = {Krebbers, Robbert}, title = {{Interactive and Automated Proofs in Modal Separation Logic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2}, URN = {urn:nbn:de:0030-drops-183770}, doi = {10.4230/LIPIcs.ITP.2023.2}, annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Niels van der Weide. The Formal Theory of Monads, Univalently. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{vanderweide:LIPIcs.FSCD.2023.6, author = {van der Weide, Niels}, title = {{The Formal Theory of Monads, Univalently}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {6:1--6:23}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.6}, URN = {urn:nbn:de:0030-drops-179904}, doi = {10.4230/LIPIcs.FSCD.2023.6}, annote = {Keywords: bicategory theory, univalent foundations, formalization, monads, Coq} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{abel:LIPIcs.TYPES.2020.1, author = {Abel, Andreas}, title = {{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {1:1--1:21}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1}, URN = {urn:nbn:de:0030-drops-138805}, doi = {10.4230/LIPIcs.TYPES.2020.1}, annote = {Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Proceedings{geuvers:LIPIcs.FSCD.2019, title = {{LIPIcs, Volume 131, FSCD'19, Complete Volume}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019}, URN = {urn:nbn:de:0030-drops-107734}, doi = {10.4230/LIPIcs.FSCD.2019}, annote = {Keywords: Theory of computation, Models of computation, Formal languages and automata theory, Logic, Semantics and reasoning} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{geuvers:LIPIcs.FSCD.2019.0, author = {Geuvers, Herman}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.0}, URN = {urn:nbn:de:0030-drops-105070}, doi = {10.4230/LIPIcs.FSCD.2019.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Beniamino Accattoli. A Fresh Look at the lambda-Calculus (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{accattoli:LIPIcs.FSCD.2019.1, author = {Accattoli, Beniamino}, title = {{A Fresh Look at the lambda-Calculus}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {1:1--1:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.1}, URN = {urn:nbn:de:0030-drops-105083}, doi = {10.4230/LIPIcs.FSCD.2019.1}, annote = {Keywords: lambda-calculus, sharing, abstract machines, type systems, rewriting} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Amy P. Felty. A Linear Logical Framework in Hybrid (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{felty:LIPIcs.FSCD.2019.2, author = {Felty, Amy P.}, title = {{A Linear Logical Framework in Hybrid}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {2:1--2:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.2}, URN = {urn:nbn:de:0030-drops-105099}, doi = {10.4230/LIPIcs.FSCD.2019.2}, annote = {Keywords: Logical frameworks, proof assistants, linear logic} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Sarah Winkler. Extending Maximal Completion (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{winkler:LIPIcs.FSCD.2019.3, author = {Winkler, Sarah}, title = {{Extending Maximal Completion}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.3}, URN = {urn:nbn:de:0030-drops-105102}, doi = {10.4230/LIPIcs.FSCD.2019.3}, annote = {Keywords: automated reasoning, completion, theorem proving} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Hongseok Yang. Some Semantic Issues in Probabilistic Programming Languages (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{yang:LIPIcs.FSCD.2019.4, author = {Yang, Hongseok}, title = {{Some Semantic Issues in Probabilistic Programming Languages}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {4:1--4:6}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.4}, URN = {urn:nbn:de:0030-drops-105118}, doi = {10.4230/LIPIcs.FSCD.2019.4}, annote = {Keywords: Probabilistic Programming, Denotational Semantics, Non-differentiable Models, Bayesian Nonparametrics, Exchangeability} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5, author = {Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels}, title = {{Bicategories in Univalent Foundations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5}, URN = {urn:nbn:de:0030-drops-105124}, doi = {10.4230/LIPIcs.FSCD.2019.5}, annote = {Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular Specification of Monads Through Higher-Order Presentations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.6, author = {Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco}, title = {{Modular Specification of Monads Through Higher-Order Presentations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.6}, URN = {urn:nbn:de:0030-drops-105136}, doi = {10.4230/LIPIcs.FSCD.2019.6}, annote = {Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Maciej Bendkowski. Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{bendkowski:LIPIcs.FSCD.2019.7, author = {Bendkowski, Maciej}, title = {{Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {7:1--7:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.7}, URN = {urn:nbn:de:0030-drops-105144}, doi = {10.4230/LIPIcs.FSCD.2019.7}, annote = {Keywords: lambda calculus, explicit substitutions, complexity, combinatorics} }
Feedback for Dagstuhl Publishing