@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}