LIPIcs, Volume 69
TYPES 2015, May 18-21, 2015, Tallinn, Estonia
Editors: Tarmo Uustalu
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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Davide Ancona, Paola Giannini, and Elena Zucca. Constrained Polymorphic Types for a Calculus with Name Variables. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{ancona_et_al:LIPIcs.TYPES.2015.4, author = {Ancona, Davide and Giannini, Paola and Zucca, Elena}, title = {{Constrained Polymorphic Types for a Calculus with Name Variables}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {4:1--4:29}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.4}, URN = {urn:nbn:de:0030-drops-84744}, doi = {10.4230/LIPIcs.TYPES.2015.4}, annote = {Keywords: open code, incremental rebinding, name polymorphism, metaprogramming} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5, author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders}, title = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {5:1--5: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5}, URN = {urn:nbn:de:0030-drops-84754}, doi = {10.4230/LIPIcs.TYPES.2015.5}, annote = {Keywords: univalence axiom, dependent type theory, cubical sets} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Juan Edi, Andrés Viso, and Eduardo Bonelli. Efficient Type Checking for Path Polymorphism. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{edi_et_al:LIPIcs.TYPES.2015.6, author = {Edi, Juan and Viso, Andr\'{e}s and Bonelli, Eduardo}, title = {{Efficient Type Checking for Path Polymorphism}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {6:1--6: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.6}, URN = {urn:nbn:de:0030-drops-84761}, doi = {10.4230/LIPIcs.TYPES.2015.6}, annote = {Keywords: lambda-calculus, pattern matching, path polymorphism, type checking} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Luca Paolini, Mauro Piccolo, and Luca Roversi. A Certified Study of a Reversible Programming Language. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{paolini_et_al:LIPIcs.TYPES.2015.7, author = {Paolini, Luca and Piccolo, Mauro and Roversi, Luca}, title = {{A Certified Study of a Reversible Programming Language}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {7:1--7:21}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.7}, URN = {urn:nbn:de:0030-drops-84771}, doi = {10.4230/LIPIcs.TYPES.2015.7}, annote = {Keywords: reversible computing, Janus, operational semantics, bi-deterministic evaluation, categorical semantics} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{parmann:LIPIcs.TYPES.2015.8, author = {Parmann, Erik}, title = {{Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {8:1--8:25}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.8}, URN = {urn:nbn:de:0030-drops-84787}, doi = {10.4230/LIPIcs.TYPES.2015.8}, annote = {Keywords: constructive logic, simplicial sets, semantics of simple types} }
Feedback for Dagstuhl Publishing