@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@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.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}
}
@InProceedings{pizaniflor_et_al:LIPIcs.TYPES.2015.9,
author = {Pizani Flor, Jo\~{a}o Paulo and Swierstra, Wouter and Sijsling, Yorick},
title = {{Pi-Ware: Hardware Description and Verification in Agda}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {9:1--9: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.9},
URN = {urn:nbn:de:0030-drops-84791},
doi = {10.4230/LIPIcs.TYPES.2015.9},
annote = {Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing