@Proceedings{matthes_et_al:LIPIcs.TYPES.2013,
  title =	{{LIPIcs, Volume 26, TYPES'13, Complete Volume}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013},
  URN =		{urn:nbn:de:0030-drops-46370},
  doi =		{10.4230/LIPIcs.TYPES.2013},
  annote =	{Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}
@InProceedings{matthes_et_al:LIPIcs.TYPES.2013.i,
  author =	{Matthes, Ralph and Schubert, Aleksy},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{i--x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.i},
  URN =		{urn:nbn:de:0030-drops-46225},
  doi =		{10.4230/LIPIcs.TYPES.2013.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{ahman_et_al:LIPIcs.TYPES.2013.1,
  author =	{Ahman, Danel and Uustalu, Tarmo},
  title =	{{Update Monads: Cointerpreting Directed Containers}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{1--23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.1},
  URN =		{urn:nbn:de:0030-drops-46235},
  doi =		{10.4230/LIPIcs.TYPES.2013.1},
  annote =	{Keywords: monads and distributive laws, reader, writer and state monads, monoids and monoid actions, directed containers}
}
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2013.24,
  author =	{Aschieri, Federico and Zorzi, Margherita},
  title =	{{A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{24--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.24},
  URN =		{urn:nbn:de:0030-drops-46245},
  doi =		{10.4230/LIPIcs.TYPES.2013.24},
  annote =	{Keywords: Markov's Principle, Intuitionistic Realizability, Heyting Arithmetic, Game Semantics}
}
@InProceedings{barthe_et_al:LIPIcs.TYPES.2013.45,
  author =	{Barthe, Gilles and Betarte, Gustavo and Campo, Juan Diego and Chimento, Jes\'{u}s Mauricio and Luna, Carlos},
  title =	{{Formally Verified Implementation of an Idealized Model of Virtualization}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{45--63},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.45},
  URN =		{urn:nbn:de:0030-drops-46254},
  doi =		{10.4230/LIPIcs.TYPES.2013.45},
  annote =	{Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation}
}
@InProceedings{berardi_et_al:LIPIcs.TYPES.2013.64,
  author =	{Berardi, Stefano and Steila, Silvia},
  title =	{{Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{64--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.64},
  URN =		{urn:nbn:de:0030-drops-46269},
  doi =		{10.4230/LIPIcs.TYPES.2013.64},
  annote =	{Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem}
}
@InProceedings{berger_et_al:LIPIcs.TYPES.2013.84,
  author =	{Berger, Ulrich and Seisenberger, Monika and Woods, Gregory J. M.},
  title =	{{Extracting Imperative Programs from Proofs: In-place Quicksort}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{84--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.84},
  URN =		{urn:nbn:de:0030-drops-46274},
  doi =		{10.4230/LIPIcs.TYPES.2013.84},
  annote =	{Keywords: Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort,Computational Monads, Minlog}
}
@InProceedings{bezem_et_al:LIPIcs.TYPES.2013.107,
  author =	{Bezem, Marc and Coquand, Thierry and Huber, Simon},
  title =	{{A Model of Type Theory in Cubical Sets}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{107--128},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107},
  URN =		{urn:nbn:de:0030-drops-46284},
  doi =		{10.4230/LIPIcs.TYPES.2013.107},
  annote =	{Keywords: Models of dependent type theory, cubical sets, Univalent Foundations}
}
@InProceedings{coppo_et_al:LIPIcs.TYPES.2013.129,
  author =	{Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Margaria, Ines and Zacchi, Maddalena},
  title =	{{Isomorphism of "Functional" Intersection Types}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{129--149},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.129},
  URN =		{urn:nbn:de:0030-drops-46296},
  doi =		{10.4230/LIPIcs.TYPES.2013.129},
  annote =	{Keywords: Type Isomorphism, Lambda calculus, Intersection Types}
}
@InProceedings{despeyroux_et_al:LIPIcs.TYPES.2013.150,
  author =	{Despeyroux, Jo\"{e}lle and Chaudhuri, Kaustuv},
  title =	{{A Hybrid Linear Logic for Constrained Transition Systems}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{150--168},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.150},
  URN =		{urn:nbn:de:0030-drops-46302},
  doi =		{10.4230/LIPIcs.TYPES.2013.150},
  annote =	{Keywords: Linear logic, hybrid logic, stochastic pi-calculus, focusing, adequacy}
}
@InProceedings{herbelin_et_al:LIPIcs.TYPES.2013.169,
  author =	{Herbelin, Hugo and Spiwack, Arnaud},
  title =	{{The Rooster and the Syntactic Bracket}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{169--187},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.169},
  URN =		{urn:nbn:de:0030-drops-46318},
  doi =		{10.4230/LIPIcs.TYPES.2013.169},
  annote =	{Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families}
}
@InProceedings{ilik_et_al:LIPIcs.TYPES.2013.188,
  author =	{Ilik, Danko and Nakata, Keiko},
  title =	{{A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{188--201},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.188},
  URN =		{urn:nbn:de:0030-drops-46320},
  doi =		{10.4230/LIPIcs.TYPES.2013.188},
  annote =	{Keywords: Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators}
}
@InProceedings{retore:LIPIcs.TYPES.2013.202,
  author =	{Retor\'{e}, Christian},
  title =	{{The Montagovian Generative Lexicon Lambda Ty\underlinen: a Type Theoretical Framework for Natural Language Semantics}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{202--229},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.202},
  URN =		{urn:nbn:de:0030-drops-46336},
  doi =		{10.4230/LIPIcs.TYPES.2013.202},
  annote =	{Keywords: type theory, computational linguistics}
}
@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230,
  author =	{Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel},
  title =	{{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{230--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230},
  URN =		{urn:nbn:de:0030-drops-46343},
  doi =		{10.4230/LIPIcs.TYPES.2013.230},
  annote =	{Keywords: Abstract Machines, Compiler Correctness, Big-step semantics}
}
@InProceedings{xue:LIPIcs.TYPES.2013.251,
  author =	{Xue, Tao},
  title =	{{Definitional Extension in Type Theory}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{251--269},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.251},
  URN =		{urn:nbn:de:0030-drops-46352},
  doi =		{10.4230/LIPIcs.TYPES.2013.251},
  annote =	{Keywords: conservative extension, definitional extension, subtype, coercive subtyping}
}