LIPIcs, Volume 69
TYPES 2015, May 18-21, 2015, Tallinn, Estonia
Editors: Tarmo Uustalu
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kesner_et_al:LIPIcs.FSCD.2024.1, author = {Kesner, Delia and Arrial, Victor and Guerrieri, Giulio}, title = {{Meaningfulness and Genericity in a Subsuming Framework}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {1:1--1: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.1}, URN = {urn:nbn:de:0030-drops-203305}, doi = {10.4230/LIPIcs.FSCD.2024.1}, annote = {Keywords: Lambda calculus, Solvability, Meaningfulness, Inhabitation, Genericity} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vanderweide:LIPIcs.FSCD.2024.4, author = {van der Weide, Niels}, title = {{Univalent Enriched Categories and the Enriched Rezk Completion}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {4:1--4:19}, 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.4}, URN = {urn:nbn:de:0030-drops-203337}, doi = {10.4230/LIPIcs.FSCD.2024.4}, annote = {Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22, author = {Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders}, title = {{Automating Boundary Filling in Cubical Agda}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {22:1--22:18}, 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.22}, URN = {urn:nbn:de:0030-drops-203514}, doi = {10.4230/LIPIcs.FSCD.2024.22}, annote = {Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23, author = {Accattoli, Beniamino and Lancelot, Adrienne}, title = {{Mirroring Call-By-Need, or Values Acting Silly}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {23:1--23: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.23}, URN = {urn:nbn:de:0030-drops-203527}, doi = {10.4230/LIPIcs.FSCD.2024.23}, annote = {Keywords: Lambda calculus, intersection types, call-by-value, call-by-need} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25, author = {Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt}, title = {{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {25:1--25:22}, 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.25}, URN = {urn:nbn:de:0030-drops-203540}, doi = {10.4230/LIPIcs.FSCD.2024.25}, annote = {Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{veltri:LIPIcs.FSCD.2021.22, author = {Veltri, Niccol\`{o}}, title = {{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22}, URN = {urn:nbn:de:0030-drops-142601}, doi = {10.4230/LIPIcs.FSCD.2021.22}, annote = {Keywords: type theory, finite powerset, final coalgebra, Cubical Agda} }
Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Danel Ahman and Tarmo Uustalu. Decomposing Comonad Morphisms. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahman_et_al:LIPIcs.CALCO.2019.14, author = {Ahman, Danel and Uustalu, Tarmo}, title = {{Decomposing Comonad Morphisms}}, booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)}, pages = {14:1--14:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-120-7}, ISSN = {1868-8969}, year = {2019}, volume = {139}, editor = {Roggenbach, Markus and Sokolova, Ana}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.14}, URN = {urn:nbn:de:0030-drops-114427}, doi = {10.4230/LIPIcs.CALCO.2019.14}, annote = {Keywords: container functors (polynomial functors), container comonads, comonad morphisms and comonad coalgebras, cofunctors, lenses} }
Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Hendrik Maarand and Tarmo Uustalu. Reordering Derivatives of Trace Closures of Regular Languages. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{maarand_et_al:LIPIcs.CONCUR.2019.40, author = {Maarand, Hendrik and Uustalu, Tarmo}, title = {{Reordering Derivatives of Trace Closures of Regular Languages}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {40:1--40:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.40}, URN = {urn:nbn:de:0030-drops-109426}, doi = {10.4230/LIPIcs.CONCUR.2019.40}, annote = {Keywords: Mazurkiewicz traces, trace closure, regular languages, finite automata, language derivatives, scattering rank, star-connected expressions} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2019.18, author = {Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s and Uustalu, Tarmo}, title = {{Modal Embeddings and Calling Paradigms}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18}, URN = {urn:nbn:de:0030-drops-105256}, doi = {10.4230/LIPIcs.FSCD.2019.18}, annote = {Keywords: intuitionistic S4, call-by-name, call-by-value, comonadic lambda-calculus, standardization, indifference property} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@Proceedings{uustalu:LIPIcs.TYPES.2015, title = {{LIPIcs, Volume 69, TYPES'15, Complete Volume}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015}, URN = {urn:nbn:de:0030-drops-86220}, doi = {10.4230/LIPIcs.TYPES.2015}, annote = {Keywords: Mathematical Logic and Formal Languages: Mathematical Logic - Lambda calculus and related systems} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{uustalu:LIPIcs.TYPES.2015.0, author = {Uustalu, Tarmo}, title = {{Front Matter, Table of Contents, Preface, External Reviewers}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {0:i--0:xii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.0}, URN = {urn:nbn:de:0030-drops-84704}, doi = {10.4230/LIPIcs.TYPES.2015.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, External Reviewers} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{adams_et_al:LIPIcs.TYPES.2015.1, author = {Adams, Robin and Jacobs, Bart}, title = {{A Type Theory for Probabilistic and Bayesian Reasoning}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {1:1--1:34}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1}, URN = {urn:nbn:de:0030-drops-84714}, doi = {10.4230/LIPIcs.TYPES.2015.1}, annote = {Keywords: Probabilistic programming, probabilistic algorithm, type theory, effect module, Bayesian reasoning} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{ahrens_et_al:LIPIcs.TYPES.2015.2, author = {Ahrens, Benedikt and Matthes, Ralph}, title = {{Heterogeneous Substitution Systems Revisited}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {2:1--2:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.2}, URN = {urn:nbn:de:0030-drops-84724}, doi = {10.4230/LIPIcs.TYPES.2015.2}, annote = {Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2015.3, author = {Altenkirch, Thorsten and Kaposi, Ambrus}, title = {{Towards a Cubical Type Theory without an Interval}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {3:1--3:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.3}, URN = {urn:nbn:de:0030-drops-84739}, doi = {10.4230/LIPIcs.TYPES.2015.3}, annote = {Keywords: homotopy type theory, parametricity, univalence} }