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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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} }
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.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} }
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.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} }
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.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} }
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} }
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.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} }