HTML Export for TYPES 2020

Copy to Clipboard Download

<h2>LIPIcs, Volume 188, TYPES 2020</h2>
<ul>
<li>
    <span class="authors">Ugo de&#039;Liguoro, Stefano Berardi, and Thorsten Altenkirch</span>
    <span class="title">LIPIcs, Volume 188, TYPES 2020, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020">10.4230/LIPIcs.TYPES.2020</a>
</li>
<li>
    <span class="authors">Ugo de&#039;Liguoro, Stefano Berardi, and Thorsten Altenkirch</span>
    <span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.0">10.4230/LIPIcs.TYPES.2020.0</a>
</li>
<li>
    <span class="authors">Andreas Abel</span>
    <span class="title">On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.1">10.4230/LIPIcs.TYPES.2020.1</a>
</li>
<li>
    <span class="authors">Reynald Affeldt and David Nowak</span>
    <span class="title">Extending Equational Monadic Reasoning with Monad Transformers</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.2">10.4230/LIPIcs.TYPES.2020.2</a>
</li>
<li>
    <span class="authors">Guido De Luca and Carlos Luna</span>
    <span class="title">Towards a Certified Reference Monitor of the Android 10 Permission System</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.3">10.4230/LIPIcs.TYPES.2020.3</a>
</li>
<li>
    <span class="authors">José Espírito Santo, Ralph Matthes, and Luís Pinto</span>
    <span class="title">Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.4">10.4230/LIPIcs.TYPES.2020.4</a>
</li>
<li>
    <span class="authors">Asta Halkjær From</span>
    <span class="title">Synthetic Completeness for a Terminating Seligman-Style Tableau System</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.5">10.4230/LIPIcs.TYPES.2020.5</a>
</li>
<li>
    <span class="authors">Gabriel Hondet and Frédéric Blanqui</span>
    <span class="title">Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.6">10.4230/LIPIcs.TYPES.2020.6</a>
</li>
<li>
    <span class="authors">Furio Honsell, Marina Lenisa, and Ivan Scagnetto</span>
    <span class="title">Λ-Symsym: An Interactive Tool for Playing with Involutions and Types</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.7">10.4230/LIPIcs.TYPES.2020.7</a>
</li>
<li>
    <span class="authors">Jasper Hugunin</span>
    <span class="title">Why Not W?</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.8">10.4230/LIPIcs.TYPES.2020.8</a>
</li>
<li>
    <span class="authors">Harry Maclean and Zhaohui Luo</span>
    <span class="title">Subtype Universes</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.9">10.4230/LIPIcs.TYPES.2020.9</a>
</li>
<li>
    <span class="authors">Matteo Manighetti, Dale Miller, and Alberto Momigliano</span>
    <span class="title">Two Applications of Logic Programming to Coq</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.10">10.4230/LIPIcs.TYPES.2020.10</a>
</li>
<li>
    <span class="authors">Paweł Urzyczyn</span>
    <span class="title">Duality in Intuitionistic Propositional Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2020.11">10.4230/LIPIcs.TYPES.2020.11</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