HTML Export for TYPES 2016

Copy to Clipboard Download

<h2>LIPIcs, Volume 97, TYPES 2016</h2>
<ul>
<li>
    <span class="authors">Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić</span>
    <span class="title">LIPIcs, Volume 97, TYPES&#039;16, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016">10.4230/LIPIcs.TYPES.2016</a>
</li>
<li>
    <span class="authors">Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic</span>
    <span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.0">10.4230/LIPIcs.TYPES.2016.0</a>
</li>
<li>
    <span class="authors">Dale Miller</span>
    <span class="title">Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.1">10.4230/LIPIcs.TYPES.2016.1</a>
</li>
<li>
    <span class="authors">Simona Ronchi Della Rocca</span>
    <span class="title">Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.2">10.4230/LIPIcs.TYPES.2016.2</a>
</li>
<li>
    <span class="authors">Robin Adams, Marc Bezem, and Thierry Coquand</span>
    <span class="title">A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.3">10.4230/LIPIcs.TYPES.2016.3</a>
</li>
<li>
    <span class="authors">Federico Aschieri and Matteo Manighetti</span>
    <span class="title">On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov&#039;s Principle in First-Order Logic and Arithmetic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.4">10.4230/LIPIcs.TYPES.2016.4</a>
</li>
<li>
    <span class="authors">Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone</span>
    <span class="title">Design and Implementation of the Andromeda Proof Assistant</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.5">10.4230/LIPIcs.TYPES.2016.5</a>
</li>
<li>
    <span class="authors">Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann</span>
    <span class="title">Realizability at Work: Separating Two Constructive Notions of Finiteness</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.6">10.4230/LIPIcs.TYPES.2016.6</a>
</li>
<li>
    <span class="authors">Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman</span>
    <span class="title">Parametricity, Automorphisms of the Universe, and Excluded Middle</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.7">10.4230/LIPIcs.TYPES.2016.7</a>
</li>
<li>
    <span class="authors">Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski</span>
    <span class="title">Coq Support in HAHA</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.8">10.4230/LIPIcs.TYPES.2016.8</a>
</li>
<li>
    <span class="authors">Lukasz Czajka</span>
    <span class="title">A Shallow Embedding of Pure Type Systems into First-Order Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.9">10.4230/LIPIcs.TYPES.2016.9</a>
</li>
<li>
    <span class="authors">José Espírito Santo, Maria João Frade, and Luís Pinto</span>
    <span class="title">Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.10">10.4230/LIPIcs.TYPES.2016.10</a>
</li>
<li>
    <span class="authors">Kuen-Bang Hou (Favonia) and Robert Harper</span>
    <span class="title">Covering Spaces in Homotopy Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.11">10.4230/LIPIcs.TYPES.2016.11</a>
</li>
<li>
    <span class="authors">Bashar Igried and Anton Setzer</span>
    <span class="title">Defining Trace Semantics for CSP-Agda</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.12">10.4230/LIPIcs.TYPES.2016.12</a>
</li>
<li>
    <span class="authors">Georgiana Elena Lungu and Zhaohui Luo</span>
    <span class="title">On Subtyping in Type Theories with Canonical Objects</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.13">10.4230/LIPIcs.TYPES.2016.13</a>
</li>
<li>
    <span class="authors">Érik Martin-Dorel and Sergei Soloviev</span>
    <span class="title">A Formal Study of Boolean Games with Random Formulas as Payoff Functions</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.14">10.4230/LIPIcs.TYPES.2016.14</a>
</li>
<li>
    <span class="authors">Richard Statman</span>
    <span class="title">The Completeness of BCD for an Operational Semantics</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2016.15">10.4230/LIPIcs.TYPES.2016.15</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