LIPIcs, Volume 175
TYPES 2019, June 11-14, 2019, Oslo, Norway
Editors: Marc Bezem and Assia Mahboubi
LIPIcs, Volume 12
CSL 2011, September 12-15, 2011, Bergen, Norway
Editors: Marc Bezem
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13, author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n}, title = {{Type Theory with Explicit Universe Polymorphism}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {13:1--13:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.13}, URN = {urn:nbn:de:0030-drops-184564}, doi = {10.4230/LIPIcs.TYPES.2022.13}, annote = {Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Michael Kohlhase, Florian Rabe, and Makarius Wenzel. Making Isabelle Content Accessible in Knowledge Representation Formats. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Sandra Alves, Delia Kesner, and Daniel Ventura. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 3:1-3:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Thorsten Altenkirch and Colin Geniet. Big Step Normalisation for Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Gun Pinyo and Nicolai Kraus. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Stefano Piceghello. Coherence for Monoidal Groupoids in HoTT. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Stefan Monnier and Nathaniel Bos. Is Impredicativity Implicitly Implicit?. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Feedback for Dagstuhl Publishing