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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{takahashi:LIPIcs.TYPES.2021.12, author = {Takahashi, Yuta}, title = {{Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {12:1--12: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.12}, URN = {urn:nbn:de:0030-drops-167811}, doi = {10.4230/LIPIcs.TYPES.2021.12}, annote = {Keywords: termination, higher-order rewriting, non-positive types, inductive types} }