@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing