@Proceedings{bezem_et_al:LIPIcs.TYPES.2019,
title = {{LIPIcs, Volume 175, TYPES 2019, Complete Volume}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {1--256},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019},
URN = {urn:nbn:de:0030-drops-130639},
doi = {10.4230/LIPIcs.TYPES.2019},
annote = {Keywords: LIPIcs, Volume 175, TYPES 2019, Complete Volume}
}
@InProceedings{bezem_et_al:LIPIcs.TYPES.2019.0,
author = {Bezem, Marc and Mahboubi, Assia},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.0},
URN = {urn:nbn:de:0030-drops-130640},
doi = {10.4230/LIPIcs.TYPES.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{kohlhase_et_al:LIPIcs.TYPES.2019.1,
author = {Kohlhase, Michael and Rabe, Florian and Wenzel, Makarius},
title = {{Making Isabelle Content Accessible in Knowledge Representation Formats}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {1:1--1:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.1},
URN = {urn:nbn:de:0030-drops-130651},
doi = {10.4230/LIPIcs.TYPES.2019.1},
annote = {Keywords: Isabelle, PIDE, OMDoc, MMT, library, export}
}
@InProceedings{cockx:LIPIcs.TYPES.2019.2,
author = {Cockx, Jesper},
title = {{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {2:1--2:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.2},
URN = {urn:nbn:de:0030-drops-130666},
doi = {10.4230/LIPIcs.TYPES.2019.2},
annote = {Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}
@InProceedings{alves_et_al:LIPIcs.TYPES.2019.3,
author = {Alves, Sandra and Kesner, Delia and Ventura, Daniel},
title = {{A Quantitative Understanding of Pattern Matching}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {3:1--3:36},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.3},
URN = {urn:nbn:de:0030-drops-130672},
doi = {10.4230/LIPIcs.TYPES.2019.3},
annote = {Keywords: Intersection Types, Pattern Matching, Exact Bounds}
}
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2019.4,
author = {Altenkirch, Thorsten and Geniet, Colin},
title = {{Big Step Normalisation for Type Theory}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.4},
URN = {urn:nbn:de:0030-drops-130682},
doi = {10.4230/LIPIcs.TYPES.2019.4},
annote = {Keywords: Normalisation, big step normalisation, type theory, dependent types, Agda}
}
@InProceedings{pinyo_et_al:LIPIcs.TYPES.2019.5,
author = {Pinyo, Gun and Kraus, Nicolai},
title = {{From Cubes to Twisted Cubes via Graph Morphisms in Type Theory}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.5},
URN = {urn:nbn:de:0030-drops-130694},
doi = {10.4230/LIPIcs.TYPES.2019.5},
annote = {Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms}
}
@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6,
author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise},
title = {{For Finitary Induction-Induction, Induction Is Enough}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {6:1--6:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.6},
URN = {urn:nbn:de:0030-drops-130707},
doi = {10.4230/LIPIcs.TYPES.2019.6},
annote = {Keywords: type theory, inductive types, inductive-inductive types}
}
@InProceedings{kravchukkirilyuk_et_al:LIPIcs.TYPES.2019.7,
author = {Kravchuk-Kirilyuk, Anastasiya and Voizard, Antoine and Weirich, Stephanie},
title = {{Eta-Equivalence in Core Dependent Haskell}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {7:1--7:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7},
URN = {urn:nbn:de:0030-drops-130716},
doi = {10.4230/LIPIcs.TYPES.2019.7},
annote = {Keywords: Dependent types, Haskell, Irrelevance, Eta-equivalence}
}
@InProceedings{piceghello:LIPIcs.TYPES.2019.8,
author = {Piceghello, Stefano},
title = {{Coherence for Monoidal Groupoids in HoTT}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {8:1--8:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8},
URN = {urn:nbn:de:0030-drops-130722},
doi = {10.4230/LIPIcs.TYPES.2019.8},
annote = {Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq}
}
@InProceedings{monnier_et_al:LIPIcs.TYPES.2019.9,
author = {Monnier, Stefan and Bos, Nathaniel},
title = {{Is Impredicativity Implicitly Implicit?}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.9},
URN = {urn:nbn:de:0030-drops-130730},
doi = {10.4230/LIPIcs.TYPES.2019.9},
annote = {Keywords: Impredicativity, Pure type systems, Inductive types, Erasable arguments, Proof irrelevance, Implicit arguments, Universe polymorphism}
}
@InProceedings{danielsson:LIPIcs.TYPES.2019.10,
author = {Danielsson, Nils Anders},
title = {{Higher Inductive Type Eliminators Without Paths}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10},
URN = {urn:nbn:de:0030-drops-130749},
doi = {10.4230/LIPIcs.TYPES.2019.10},
annote = {Keywords: Cubical Agda, higher 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