@Proceedings{ghilezan_et_al:LIPIcs.TYPES.2016,
  title =	{{LIPIcs, Volume 97, TYPES'16, Complete Volume}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016},
  URN =		{urn:nbn:de:0030-drops-98651},
  doi =		{10.4230/LIPIcs.TYPES.2016},
  annote =	{Keywords: Theory of computation, Type theory}
}
@InProceedings{ghilezan_et_al:LIPIcs.TYPES.2016.0,
  author =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.0},
  URN =		{urn:nbn:de:0030-drops-98466},
  doi =		{10.4230/LIPIcs.TYPES.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{miller:LIPIcs.TYPES.2016.1,
  author =	{Miller, Dale},
  title =	{{Mechanized Metatheory Revisited: An Extended Abstract}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{1:1--1:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.1},
  URN =		{urn:nbn:de:0030-drops-98603},
  doi =		{10.4230/LIPIcs.TYPES.2016.1},
  annote =	{Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax}
}
@InProceedings{ronchidellarocca:LIPIcs.TYPES.2016.2,
  author =	{Ronchi Della Rocca, Simona},
  title =	{{Intersection Types and Denotational Semantics: An Extended Abstract}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{2:1--2:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.2},
  URN =		{urn:nbn:de:0030-drops-98614},
  doi =		{10.4230/LIPIcs.TYPES.2016.2},
  annote =	{Keywords: Lambda-calculus, Lambda-models, Intersection types}
}
@InProceedings{adams_et_al:LIPIcs.TYPES.2016.3,
  author =	{Adams, Robin and Bezem, Marc and Coquand, Thierry},
  title =	{{A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.3},
  URN =		{urn:nbn:de:0030-drops-98581},
  doi =		{10.4230/LIPIcs.TYPES.2016.3},
  annote =	{Keywords: type theory, univalence, canonicity}
}
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2016.4,
  author =	{Aschieri, Federico and Manighetti, Matteo},
  title =	{{On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4},
  URN =		{urn:nbn:de:0030-drops-98590},
  doi =		{10.4230/LIPIcs.TYPES.2016.4},
  annote =	{Keywords: Markov's Principle, first-order logic, natural deduction, Curry-Howard}
}
@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5,
  author =	{Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.},
  title =	{{Design and Implementation of the Andromeda Proof Assistant}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{5:1--5:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5},
  URN =		{urn:nbn:de:0030-drops-98574},
  doi =		{10.4230/LIPIcs.TYPES.2016.5},
  annote =	{Keywords: type theory, proof assistant, equality reflection, computational effects}
}
@InProceedings{bezem_et_al:LIPIcs.TYPES.2016.6,
  author =	{Bezem, Marc and Coquand, Thierry and Nakata, Keiko and Parmann, Erik},
  title =	{{Realizability at Work: Separating Two Constructive Notions of Finiteness}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.6},
  URN =		{urn:nbn:de:0030-drops-98541},
  doi =		{10.4230/LIPIcs.TYPES.2016.6},
  annote =	{Keywords: Type theory, realizability, constructive notions of finiteness}
}
@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7,
  author =	{Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael},
  title =	{{Parametricity, Automorphisms of the Universe, and Excluded Middle}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{7:1--7:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7},
  URN =		{urn:nbn:de:0030-drops-98554},
  doi =		{10.4230/LIPIcs.TYPES.2016.7},
  annote =	{Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat}
}
@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8,
  author =	{Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub},
  title =	{{Coq Support in HAHA}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{8:1--8:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8},
  URN =		{urn:nbn:de:0030-drops-98562},
  doi =		{10.4230/LIPIcs.TYPES.2016.8},
  annote =	{Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}
@InProceedings{czajka:LIPIcs.TYPES.2016.9,
  author =	{Czajka, Lukasz},
  title =	{{A Shallow Embedding of Pure Type Systems into First-Order Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{9:1--9:39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9},
  URN =		{urn:nbn:de:0030-drops-98533},
  doi =		{10.4230/LIPIcs.TYPES.2016.9},
  annote =	{Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory}
}
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2016.10,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Frade, Maria Jo\~{a}o and Pinto, Lu{\'\i}s},
  title =	{{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{10:1--10:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.10},
  URN =		{urn:nbn:de:0030-drops-98523},
  doi =		{10.4230/LIPIcs.TYPES.2016.10},
  annote =	{Keywords: sequent calculus, permutative conversion, Curry-Howard isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli}
}
@InProceedings{hou(favonia)_et_al:LIPIcs.TYPES.2016.11,
  author =	{Hou (Favonia), Kuen-Bang and Harper, Robert},
  title =	{{Covering Spaces in Homotopy Type Theory}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.11},
  URN =		{urn:nbn:de:0030-drops-98512},
  doi =		{10.4230/LIPIcs.TYPES.2016.11},
  annote =	{Keywords: homotopy type theory, covering space, fundamental group, mechanized reasoning}
}
@InProceedings{igried_et_al:LIPIcs.TYPES.2016.12,
  author =	{Igried, Bashar and Setzer, Anton},
  title =	{{Defining Trace Semantics for CSP-Agda}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.12},
  URN =		{urn:nbn:de:0030-drops-98509},
  doi =		{10.4230/LIPIcs.TYPES.2016.12},
  annote =	{Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming,}
}
@InProceedings{lungu_et_al:LIPIcs.TYPES.2016.13,
  author =	{Lungu, Georgiana Elena and Luo, Zhaohui},
  title =	{{On Subtyping in Type Theories with Canonical Objects}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{13:1--13:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.13},
  URN =		{urn:nbn:de:0030-drops-98496},
  doi =		{10.4230/LIPIcs.TYPES.2016.13},
  annote =	{Keywords: subtyping, type theory, conservative extension, canonical objects}
}
@InProceedings{martindorel_et_al:LIPIcs.TYPES.2016.14,
  author =	{Martin-Dorel, \'{E}rik and Soloviev, Sergei},
  title =	{{A Formal Study of Boolean Games with Random Formulas as Payoff Functions}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{14:1--14:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.14},
  URN =		{urn:nbn:de:0030-drops-98486},
  doi =		{10.4230/LIPIcs.TYPES.2016.14},
  annote =	{Keywords: Boolean games, Random process, Coq formal proofs}
}
@InProceedings{statman:LIPIcs.TYPES.2016.15,
  author =	{Statman, Richard},
  title =	{{The Completeness of BCD for an Operational Semantics}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{15:1--15:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.15},
  URN =		{urn:nbn:de:0030-drops-98478},
  doi =		{10.4230/LIPIcs.TYPES.2016.15},
  annote =	{Keywords: intersection types, operational semantics, Beth model, logical relations, forcing}
}