HTML Export for TYPES 2019

Copy to Clipboard Download

<h2>LIPIcs, Volume 175, TYPES 2019</h2>
<ul>
<li>
    <span class="authors">Marc Bezem and Assia Mahboubi</span>
    <span class="title">LIPIcs, Volume 175, TYPES 2019, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019">10.4230/LIPIcs.TYPES.2019</a>
</li>
<li>
    <span class="authors">Marc Bezem and Assia Mahboubi</span>
    <span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.0">10.4230/LIPIcs.TYPES.2019.0</a>
</li>
<li>
    <span class="authors">Michael Kohlhase, Florian Rabe, and Makarius Wenzel</span>
    <span class="title">Making Isabelle Content Accessible in Knowledge Representation Formats</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.1">10.4230/LIPIcs.TYPES.2019.1</a>
</li>
<li>
    <span class="authors">Jesper Cockx</span>
    <span class="title">Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.2">10.4230/LIPIcs.TYPES.2019.2</a>
</li>
<li>
    <span class="authors">Sandra Alves, Delia Kesner, and Daniel Ventura</span>
    <span class="title">A Quantitative Understanding of Pattern Matching</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.3">10.4230/LIPIcs.TYPES.2019.3</a>
</li>
<li>
    <span class="authors">Thorsten Altenkirch and Colin Geniet</span>
    <span class="title">Big Step Normalisation for Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.4">10.4230/LIPIcs.TYPES.2019.4</a>
</li>
<li>
    <span class="authors">Gun Pinyo and Nicolai Kraus</span>
    <span class="title">From Cubes to Twisted Cubes via Graph Morphisms in Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.5">10.4230/LIPIcs.TYPES.2019.5</a>
</li>
<li>
    <span class="authors">Ambrus Kaposi, András Kovács, and Ambroise Lafont</span>
    <span class="title">For Finitary Induction-Induction, Induction Is Enough</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.6">10.4230/LIPIcs.TYPES.2019.6</a>
</li>
<li>
    <span class="authors">Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich</span>
    <span class="title">Eta-Equivalence in Core Dependent Haskell</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.7">10.4230/LIPIcs.TYPES.2019.7</a>
</li>
<li>
    <span class="authors">Stefano Piceghello</span>
    <span class="title">Coherence for Monoidal Groupoids in HoTT</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.8">10.4230/LIPIcs.TYPES.2019.8</a>
</li>
<li>
    <span class="authors">Stefan Monnier and Nathaniel Bos</span>
    <span class="title">Is Impredicativity Implicitly Implicit?</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.9">10.4230/LIPIcs.TYPES.2019.9</a>
</li>
<li>
    <span class="authors">Nils Anders Danielsson</span>
    <span class="title">Higher Inductive Type Eliminators Without Paths</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2019.10">10.4230/LIPIcs.TYPES.2019.10</a>
</li>
</ul>

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