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 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10, author = {Kaposi, Ambrus and Xie, Szumi}, title = {{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {10:1--10:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, URN = {urn:nbn:de:0030-drops-203396}, doi = {10.4230/LIPIcs.FSCD.2024.10}, annote = {Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kavvos:LIPIcs.FSCD.2024.14, author = {Kavvos, G. A.}, title = {{Two-Dimensional Kripke Semantics I: Presheaves}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {14:1--14:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14}, URN = {urn:nbn:de:0030-drops-203438}, doi = {10.4230/LIPIcs.FSCD.2024.14}, annote = {Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Mikołaj Bojańczyk, Lê Thành Dũng (Tito) Nguyễn, and Rafał Stefański. Function Spaces for Orbit-Finite Sets. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 130:1-130:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2024.130, author = {Boja\'{n}czyk, Miko{\l}aj and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Stefa\'{n}ski, Rafa{\l}}, title = {{Function Spaces for Orbit-Finite Sets}}, booktitle = {51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)}, pages = {130:1--130:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-322-5}, ISSN = {1868-8969}, year = {2024}, volume = {297}, editor = {Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.130}, URN = {urn:nbn:de:0030-drops-202730}, doi = {10.4230/LIPIcs.ICALP.2024.130}, annote = {Keywords: Orbit-finite sets, automata, linear types, game semantics} }
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} }