HTML Export for TYPES 2014

Copy to Clipboard Download

<h2>LIPIcs, Volume 39, TYPES 2014</h2>
<ul>
<li>
    <span class="authors">Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau</span>
    <span class="title">LIPIcs, Volume 39, TYPES&#039;14, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014">10.4230/LIPIcs.TYPES.2014</a>
</li>
<li>
    <span class="authors">Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau</span>
    <span class="title">Front Matter, Table of Contents, Preface, Authors Index</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.i">10.4230/LIPIcs.TYPES.2014.i</a>
</li>
<li>
    <span class="authors">Benedikt Ahrens and Régis Spadotti</span>
    <span class="title">Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.1">10.4230/LIPIcs.TYPES.2014.1</a>
</li>
<li>
    <span class="authors">Ali Assaf</span>
    <span class="title">A Calculus of Constructions with Explicit Subtyping</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.27">10.4230/LIPIcs.TYPES.2014.27</a>
</li>
<li>
    <span class="authors">Raphaël Cauderlier and Catherine Dubois</span>
    <span class="title">Objects and Subtyping in the Lambda-Pi-Calculus Modulo</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.47">10.4230/LIPIcs.TYPES.2014.47</a>
</li>
<li>
    <span class="authors">Olivier Danvy, Chantal Keller, and Matthias Puech</span>
    <span class="title">Typeful Normalization by Evaluation</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.72">10.4230/LIPIcs.TYPES.2014.72</a>
</li>
<li>
    <span class="authors">Jules Hedges</span>
    <span class="title">Dialectica Categories and Games with Bidding</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.89">10.4230/LIPIcs.TYPES.2014.89</a>
</li>
<li>
    <span class="authors">Nicolai Kraus</span>
    <span class="title">The General Universal Property of the Propositional Truncation</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.111">10.4230/LIPIcs.TYPES.2014.111</a>
</li>
<li>
    <span class="authors">Jean-Louis Krivine</span>
    <span class="title">On the Structure of Classical Realizability Models of ZF</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.146">10.4230/LIPIcs.TYPES.2014.146</a>
</li>
<li>
    <span class="authors">Maria Emilia Maietti and Samuele Maschio</span>
    <span class="title">An Extensional Kleene Realizability Semantics for the Minimalist Foundation</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.162">10.4230/LIPIcs.TYPES.2014.162</a>
</li>
<li>
    <span class="authors">Erik Parmann</span>
    <span class="title">Investigating Streamless Sets</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.187">10.4230/LIPIcs.TYPES.2014.187</a>
</li>
<li>
    <span class="authors">Andrew M. Pitts</span>
    <span class="title">Nominal Presentation of Cubical Sets Models of Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.202">10.4230/LIPIcs.TYPES.2014.202</a>
</li>
<li>
    <span class="authors">Andrew Polonsky</span>
    <span class="title">Extensionality of lambda-*</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.221">10.4230/LIPIcs.TYPES.2014.221</a>
</li>
<li>
    <span class="authors">Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz</span>
    <span class="title">Restricted Positive Quantification Is Not Elementary</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.251">10.4230/LIPIcs.TYPES.2014.251</a>
</li>
<li>
    <span class="authors">Sergei Soloviev</span>
    <span class="title">On Isomorphism of Dependent Products in a Typed Logical Framework</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.274">10.4230/LIPIcs.TYPES.2014.274</a>
</li>
<li>
    <span class="authors">Silvia Steila</span>
    <span class="title">An Intuitionistic Analysis of Size-change Termination</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2014.288">10.4230/LIPIcs.TYPES.2014.288</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