LIPIcs, Volume 130
TYPES 2018, June 18-21, 2018, Braga, Portugal
Editors: Peter Dybjer, José Espírito Santo, and Luís Pinto
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.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 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14, author = {Zeuner, Max and M\"{o}rtberg, Anders}, title = {{A Univalent Formalization of Constructive Affine Schemes}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {14:1--14:24}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14}, URN = {urn:nbn:de:0030-drops-184574}, doi = {10.4230/LIPIcs.TYPES.2022.14}, annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics} }
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.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 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018, title = {{LIPIcs, Volume 130, TYPES'18, Complete Volume}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018}, URN = {urn:nbn:de:0030-drops-114507}, doi = {10.4230/LIPIcs.TYPES.2018}, annote = {Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0, author = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0}, URN = {urn:nbn:de:0030-drops-114045}, doi = {10.4230/LIPIcs.TYPES.2018.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1, author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton}, title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1}, URN = {urn:nbn:de:0030-drops-114052}, doi = {10.4230/LIPIcs.TYPES.2018.1}, annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{A Simpler Undecidability Proof for System F Inhabitation}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {2:1--2:11}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2}, URN = {urn:nbn:de:0030-drops-114061}, doi = {10.4230/LIPIcs.TYPES.2018.2}, annote = {Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{petrakis:LIPIcs.TYPES.2018.3, author = {Petrakis, Iosif}, title = {{Dependent Sums and Dependent Products in Bishop’s Set Theory}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {3:1--3:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3}, URN = {urn:nbn:de:0030-drops-114070}, doi = {10.4230/LIPIcs.TYPES.2018.3}, annote = {Keywords: Bishop’s constructive mathematics, Martin-L\"{o}f’s type theory, dependent sums, dependent products, type-theoretic axiom of choice} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca. Semantic Subtyping for Non-Strict Languages. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{petrucciani_et_al:LIPIcs.TYPES.2018.4, author = {Petrucciani, Tommaso and Castagna, Giuseppe and Ancona, Davide and Zucca, Elena}, title = {{Semantic Subtyping for Non-Strict Languages}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {4:1--4:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.4}, URN = {urn:nbn:de:0030-drops-114083}, doi = {10.4230/LIPIcs.TYPES.2018.4}, annote = {Keywords: Semantic subtyping, non-strict semantics, call-by-need, union types, intersection types} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Anders Schlichtkrull. New Formalized Results on the Meta-Theory of a Paraconsistent Logic. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{schlichtkrull:LIPIcs.TYPES.2018.5, author = {Schlichtkrull, Anders}, title = {{New Formalized Results on the Meta-Theory of a Paraconsistent Logic}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {5:1--5:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.5}, URN = {urn:nbn:de:0030-drops-114098}, doi = {10.4230/LIPIcs.TYPES.2018.5}, annote = {Keywords: Paraconsistent logic, Many-valued logic, Formalization, Isabelle proof assistant, Paraconsistency} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{sestini:LIPIcs.TYPES.2018.6, author = {Sestini, Filippo}, title = {{Normalization by Evaluation for Typed Weak lambda-Reduction}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {6:1--6:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6}, URN = {urn:nbn:de:0030-drops-114101}, doi = {10.4230/LIPIcs.TYPES.2018.6}, annote = {Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Taichi Uemura. Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{uemura:LIPIcs.TYPES.2018.7, author = {Uemura, Taichi}, title = {{Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {7:1--7:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.7}, URN = {urn:nbn:de:0030-drops-114118}, doi = {10.4230/LIPIcs.TYPES.2018.7}, annote = {Keywords: Cubical type theory, Realizability, Impredicative universe, Univalence, Propositional resizing} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138, author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter}, title = {{Undecidability of Equality in the Free Locally Cartesian Closed Category}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {138--152}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138}, URN = {urn:nbn:de:0030-drops-51602}, doi = {10.4230/LIPIcs.TLCA.2015.138}, annote = {Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Gilles Barthe, Peter Dybjer, and Peter Thiemann. Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341). Dagstuhl Seminar Report 317, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)
@TechReport{barthe_et_al:DagSemRep.317, author = {Barthe, Gilles and Dybjer, Peter and Thiemann, Peter}, title = {{Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341)}}, pages = {1--13}, ISSN = {1619-0203}, year = {2002}, type = {Dagstuhl Seminar Report}, number = {317}, institution = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.317}, URN = {urn:nbn:de:0030-drops-152017}, doi = {10.4230/DagSemRep.317}, }
Feedback for Dagstuhl Publishing