BibTeX Export for TYPES 2017

Copy to Clipboard Download

@Proceedings{abel_et_al:LIPIcs.TYPES.2017,
  title =	{{LIPIcs, Volume 104, TYPES'17, Complete Volume}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017},
  URN =		{urn:nbn:de:0030-drops-101671},
  doi =		{10.4230/LIPIcs.TYPES.2017},
  annote =	{Keywords: Theory of computation, Type theory, Proof theory, Program verification}
}
@InProceedings{abel_et_al:LIPIcs.TYPES.2017.0,
  author =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.0},
  URN =		{urn:nbn:de:0030-drops-100488},
  doi =		{10.4230/LIPIcs.TYPES.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{allais:LIPIcs.TYPES.2017.1,
  author =	{Allais, Guillaume},
  title =	{{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.1},
  URN =		{urn:nbn:de:0030-drops-100490},
  doi =		{10.4230/LIPIcs.TYPES.2017.1},
  annote =	{Keywords: Type System, Bidirectional, Linear Logic, Agda}
}
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{Lower End of the Linial-Post Spectrum}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{2:1--2:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.2},
  URN =		{urn:nbn:de:0030-drops-100503},
  doi =		{10.4230/LIPIcs.TYPES.2017.2},
  annote =	{Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type}
}
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2017.3,
  author =	{Geuvers, Herman and Hurkens, Tonny},
  title =	{{Proof Terms for Generalized Natural Deduction}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{3:1--3:39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.3},
  URN =		{urn:nbn:de:0030-drops-100519},
  doi =		{10.4230/LIPIcs.TYPES.2017.3},
  annote =	{Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism}
}
@InProceedings{lepigre:LIPIcs.TYPES.2017.4,
  author =	{Lepigre, Rodolphe},
  title =	{{PML2: Integrated Program Verification in ML}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{4:1--4:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.4},
  URN =		{urn:nbn:de:0030-drops-100521},
  doi =		{10.4230/LIPIcs.TYPES.2017.4},
  annote =	{Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping}
}
@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5,
  author =	{Michaelis, Julius and Nipkow, Tobias},
  title =	{{Formalized Proof Systems for Propositional Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5},
  URN =		{urn:nbn:de:0030-drops-100537},
  doi =		{10.4230/LIPIcs.TYPES.2017.5},
  annote =	{Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution}
}
@InProceedings{orton_et_al:LIPIcs.TYPES.2017.6,
  author =	{Orton, Ian and Pitts, Andrew M.},
  title =	{{Decomposing the Univalence Axiom}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.6},
  URN =		{urn:nbn:de:0030-drops-100546},
  doi =		{10.4230/LIPIcs.TYPES.2017.6},
  annote =	{Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets}
}
@InProceedings{palmgren:LIPIcs.TYPES.2017.7,
  author =	{Palmgren, Erik},
  title =	{{On Equality of Objects in Categories in Constructive Type Theory}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{7:1--7:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.7},
  URN =		{urn:nbn:de:0030-drops-100553},
  doi =		{10.4230/LIPIcs.TYPES.2017.7},
  annote =	{Keywords: type theory, formalization, category theory, setoids}
}

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