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 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)
Henning Basold, Jesper Cockx, and Silvia Ghilezan. LIPIcs, Volume 239, TYPES 2021, Complete Volume. In 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)
Henning Basold, Jesper Cockx, and Silvia Ghilezan. Front Matter, Table of Contents, Preface, Conference Organization. In 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} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Christa Jenkins, Andrew Marmaduke, and Aaron Stump. Simulating Large Eliminations in Cedille. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 9:1-9:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{jenkins_et_al:LIPIcs.TYPES.2021.9, author = {Jenkins, Christa and Marmaduke, Andrew and Stump, Aaron}, title = {{Simulating Large Eliminations in Cedille}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {9:1--9:22}, 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.9}, URN = {urn:nbn:de:0030-drops-167784}, doi = {10.4230/LIPIcs.TYPES.2021.9}, annote = {Keywords: large eliminations, generic programming, impredicative encodings, Cedille, Mendler algebra} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 10:1-10:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{nakov_et_al:LIPIcs.TYPES.2021.10, author = {Nakov, Georgi and Nordvall Forsberg, Fredrik}, title = {{Quantitative Polynomial Functors}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {10:1--10:22}, 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.10}, URN = {urn:nbn:de:0030-drops-167795}, doi = {10.4230/LIPIcs.TYPES.2021.10}, annote = {Keywords: quantitative type theory, polynomial functors, inductive data types} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 11:1-11:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{paulus_et_al:LIPIcs.TYPES.2021.11, author = {Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.}, title = {{Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {11:1--11: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.11}, URN = {urn:nbn:de:0030-drops-167808}, doi = {10.4230/LIPIcs.TYPES.2021.11}, annote = {Keywords: Resource \lambda-calculus, intersection types, session types, process calculi} }
Feedback for Dagstuhl Publishing