LIPIcs, Volume 260
FSCD 2023, July 3-6, 2023, Rome, Italy
Editors: Marco Gaboardi and Femke van Raamsdonk
LIPIcs, Volume 21
RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands
Editors: Femke van Raamsdonk
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2024.1, author = {Kesner, Delia and Arrial, Victor and Guerrieri, Giulio}, title = {{Meaningfulness and Genericity in a Subsuming Framework}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {1:1--1:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.1}, URN = {urn:nbn:de:0030-drops-203305}, doi = {10.4230/LIPIcs.FSCD.2024.1}, annote = {Keywords: Lambda calculus, Solvability, Meaningfulness, Inhabitation, Genericity} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vanderweide:LIPIcs.FSCD.2024.4, author = {van der Weide, Niels}, title = {{Univalent Enriched Categories and the Enriched Rezk Completion}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {4:1--4:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.4}, URN = {urn:nbn:de:0030-drops-203337}, doi = {10.4230/LIPIcs.FSCD.2024.4}, annote = {Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Andrej Dudenhefner and Daniele Pautasso. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2024.8, author = {Dudenhefner, Andrej and Pautasso, Daniele}, title = {{Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {8:1--8:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.8}, URN = {urn:nbn:de:0030-drops-203371}, doi = {10.4230/LIPIcs.FSCD.2024.8}, annote = {Keywords: lambda-calculus, simple types, intersection types, strong normalization, mechanization, perpetual reductions} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10, author = {Kaposi, Ambrus and Xie, Szumi}, title = {{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {10:1--10:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, URN = {urn:nbn:de:0030-drops-203396}, doi = {10.4230/LIPIcs.FSCD.2024.10}, annote = {Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21, author = {Felicissimo, Thiago and Winterhalter, Th\'{e}o}, title = {{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {21:1--21:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21}, URN = {urn:nbn:de:0030-drops-203503}, doi = {10.4230/LIPIcs.FSCD.2024.21}, annote = {Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1-658, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@Proceedings{gaboardi_et_al:LIPIcs.FSCD.2023, title = {{LIPIcs, Volume 260, FSCD 2023, Complete Volume}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {1--658}, 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}, URN = {urn:nbn:de:0030-drops-179830}, doi = {10.4230/LIPIcs.FSCD.2023}, annote = {Keywords: LIPIcs, Volume 260, FSCD 2023, Complete Volume} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{gaboardi_et_al:LIPIcs.FSCD.2023.0, author = {Gaboardi, Marco and van Raamsdonk, Femke}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {0:i--0:xviii}, 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.0}, URN = {urn:nbn:de:0030-drops-179849}, doi = {10.4230/LIPIcs.FSCD.2023.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Maribel Fernández. Nominal Techniques for Software Specification and Verification (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{fernandez:LIPIcs.FSCD.2023.1, author = {Fern\'{a}ndez, Maribel}, title = {{Nominal Techniques for Software Specification and Verification}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {1:1--1:4}, 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.1}, URN = {urn:nbn:de:0030-drops-179855}, doi = {10.4230/LIPIcs.FSCD.2023.1}, annote = {Keywords: Binding operator, Nominal Logic, Nominal Rewriting, Unification, Equational Theories, Type Systems} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Mateja Jamnik. How Can We Make Trustworthy AI? (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{jamnik:LIPIcs.FSCD.2023.2, author = {Jamnik, Mateja}, title = {{How Can We Make Trustworthy AI?}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {2:1--2:1}, 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.2}, URN = {urn:nbn:de:0030-drops-179869}, doi = {10.4230/LIPIcs.FSCD.2023.2}, annote = {Keywords: AI, human-centric computing, knowledge representation, reasoning, machine learning} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Giulio Manzonetto. A Lambda Calculus Satellite (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{manzonetto:LIPIcs.FSCD.2023.3, author = {Manzonetto, Giulio}, title = {{A Lambda Calculus Satellite}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {3:1--3:14}, 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.3}, URN = {urn:nbn:de:0030-drops-179878}, doi = {10.4230/LIPIcs.FSCD.2023.3}, annote = {Keywords: \lambda-calculus, rewriting, denotational models, equational theories} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Akihisa Yamada. Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{yamada:LIPIcs.FSCD.2023.4, author = {Yamada, Akihisa}, title = {{Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {4:1--4:5}, 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.4}, URN = {urn:nbn:de:0030-drops-179882}, doi = {10.4230/LIPIcs.FSCD.2023.4}, annote = {Keywords: Term rewriting, Termination, Isabelle/HOL, Competition} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{uemura:LIPIcs.FSCD.2023.5, author = {Uemura, Taichi}, title = {{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {5:1--5:19}, 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.5}, URN = {urn:nbn:de:0030-drops-179897}, doi = {10.4230/LIPIcs.FSCD.2023.5}, annote = {Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation} }
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.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} }