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} }
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} }
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} }
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} }
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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-Ware: Hardware Description and Verification in Agda. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 9:1-9:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }