LIPIcs, Volume 239
TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)
Editors: Henning Basold, Jesper Cockx, and Silvia Ghilezan
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{basold_et_al:LIPIcs.ITP.2024.8, author = {Basold, Henning and Bruin, Peter and Lawson, Dominique}, title = {{The Directed Van Kampen Theorem in Lean}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8}, URN = {urn:nbn:de:0030-drops-207368}, doi = {10.4230/LIPIcs.ITP.2024.8}, annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Lorenzo Clemente. Weighted Basic Parallel Processes and Combinatorial Enumeration. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clemente:LIPIcs.CONCUR.2024.18, author = {Clemente, Lorenzo}, title = {{Weighted Basic Parallel Processes and Combinatorial Enumeration}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {18:1--18:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.18}, URN = {urn:nbn:de:0030-drops-207903}, doi = {10.4230/LIPIcs.CONCUR.2024.18}, annote = {Keywords: weighted automata, combinatorial enumeration, shuffle, algebraic differential equations, process algebra, basic parallel processes, species of structures} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25, author = {Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt}, title = {{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {25:1--25:22}, 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.25}, URN = {urn:nbn:de:0030-drops-203540}, doi = {10.4230/LIPIcs.FSCD.2024.25}, annote = {Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library} }
Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Henning Basold and Tanjona Ralaivaosaona. Composition and Recursion for Causal Structures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{basold_et_al:LIPIcs.CALCO.2023.18, author = {Basold, Henning and Ralaivaosaona, Tanjona}, title = {{Composition and Recursion for Causal Structures}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {18:1--18:17}, 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.18}, URN = {urn:nbn:de:0030-drops-188157}, doi = {10.4230/LIPIcs.CALCO.2023.18}, annote = {Keywords: Causal morphisms, Final Coalgebras, Final Chains, Metric Maps, Guarded Recursion, Traced Symmetric Monoidal Category} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@Proceedings{basold_et_al:LIPIcs.TYPES.2021, title = {{LIPIcs, Volume 239, TYPES 2021, Complete Volume}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {1--280}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021}, URN = {urn:nbn:de:0030-drops-167680}, doi = {10.4230/LIPIcs.TYPES.2021}, annote = {Keywords: LIPIcs, Volume 239, TYPES 2021, Complete Volume} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{basold_et_al:LIPIcs.TYPES.2021.0, author = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {0:i--0:viii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.0}, URN = {urn:nbn:de:0030-drops-167691}, doi = {10.4230/LIPIcs.TYPES.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1:1-1:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{alhabardi_et_al:LIPIcs.TYPES.2021.1, author = {Alhabardi, Fahad F. and Beckmann, Arnold and Lazar, Bogdan and Setzer, Anton}, title = {{Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {1:1--1:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.1}, URN = {urn:nbn:de:0030-drops-167704}, doi = {10.4230/LIPIcs.TYPES.2021.1}, annote = {Keywords: Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, Bitcoin Script, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics, Provable correctness, Symbolic execution, Smart contracts} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Thibaut Benjamin. Formalisation of Dependent Type Theory: The Example of CaTT. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{benjamin:LIPIcs.TYPES.2021.2, author = {Benjamin, Thibaut}, title = {{Formalisation of Dependent Type Theory: The Example of CaTT}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {2:1--2:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.2}, URN = {urn:nbn:de:0030-drops-167719}, doi = {10.4230/LIPIcs.TYPES.2021.2}, annote = {Keywords: Dependent type theory, homotopy type theory, higher categories, formalisation, Agda, proof assistant} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Rafaël Bocquet. Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 3:1-3:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{bocquet:LIPIcs.TYPES.2021.3, author = {Bocquet, Rafa\"{e}l}, title = {{Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {3:1--3:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.3}, URN = {urn:nbn:de:0030-drops-167724}, doi = {10.4230/LIPIcs.TYPES.2021.3}, annote = {Keywords: type theory, strictification, coherence, familial representability, unification} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
William DeMeo and Jacques Carette. A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{demeo_et_al:LIPIcs.TYPES.2021.4, author = {DeMeo, William and Carette, Jacques}, title = {{A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-L\"{o}f Type Theory}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {4:1--4:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.4}, URN = {urn:nbn:de:0030-drops-167737}, doi = {10.4230/LIPIcs.TYPES.2021.4}, annote = {Keywords: Agda, constructive mathematics, dependent types, equational logic, formal verification, Martin-L\"{o}f type theory, model theory, universal algebra} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Pietro Di Gianantonio and Marina Lenisa. Principal Types as Lambda Nets. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{digianantonio_et_al:LIPIcs.TYPES.2021.5, author = {Di Gianantonio, Pietro and Lenisa, Marina}, title = {{Principal Types as Lambda Nets}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {5:1--5:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.5}, URN = {urn:nbn:de:0030-drops-167744}, doi = {10.4230/LIPIcs.TYPES.2021.5}, annote = {Keywords: Lambda calculus, Principal types, Linear logic, Lambda nets, Normalization, Cut elimination} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
István Donkó and Ambrus Kaposi. Internal Strict Propositions Using Point-Free Equations. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{donko_et_al:LIPIcs.TYPES.2021.6, author = {Donk\'{o}, Istv\'{a}n and Kaposi, Ambrus}, title = {{Internal Strict Propositions Using Point-Free Equations}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {6:1--6:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.6}, URN = {urn:nbn:de:0030-drops-167759}, doi = {10.4230/LIPIcs.TYPES.2021.6}, annote = {Keywords: Martin-L\"{o}f’s type theory, intensional type theory, function extensionality, setoid model, homotopy type theory} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Constructive Cut Elimination in Geometric Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{fellin_et_al:LIPIcs.TYPES.2021.7, author = {Fellin, Giulio and Negri, Sara and Orlandelli, Eugenio}, title = {{Constructive Cut Elimination in Geometric Logic}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {7:1--7:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.7}, URN = {urn:nbn:de:0030-drops-167763}, doi = {10.4230/LIPIcs.TYPES.2021.7}, annote = {Keywords: Geometric theories, sequent calculi, axioms-as-rules, infinitary logic, constructive cut elimination} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Asta Halkjær From. A Succinct Formalization of the Completeness of First-Order Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{from:LIPIcs.TYPES.2021.8, author = {From, Asta Halkj{\ae}r}, title = {{A Succinct Formalization of the Completeness of First-Order Logic}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {8:1--8:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.8}, URN = {urn:nbn:de:0030-drops-167771}, doi = {10.4230/LIPIcs.TYPES.2021.8}, annote = {Keywords: First-Order Logic, Completeness, Isabelle/HOL} }
Feedback for Dagstuhl Publishing