HTML Export for TYPES 2013

Copy to Clipboard Download

<h2>LIPIcs, Volume 26, TYPES 2013</h2>
<ul>
<li>
    <span class="authors">Ralph Matthes and Aleksy Schubert</span>
    <span class="title">LIPIcs, Volume 26, TYPES&#039;13, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013">10.4230/LIPIcs.TYPES.2013</a>
</li>
<li>
    <span class="authors">Ralph Matthes and Aleksy Schubert</span>
    <span class="title">Frontmatter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.i">10.4230/LIPIcs.TYPES.2013.i</a>
</li>
<li>
    <span class="authors">Danel Ahman and Tarmo Uustalu</span>
    <span class="title">Update Monads: Cointerpreting Directed Containers</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.1">10.4230/LIPIcs.TYPES.2013.1</a>
</li>
<li>
    <span class="authors">Federico Aschieri and Margherita Zorzi</span>
    <span class="title">A &quot;Game Semantical&quot; Intuitionistic Realizability Validating Markov&#039;s Principle</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.24">10.4230/LIPIcs.TYPES.2013.24</a>
</li>
<li>
    <span class="authors">Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna</span>
    <span class="title">Formally Verified Implementation of an Idealized Model of Virtualization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.45">10.4230/LIPIcs.TYPES.2013.45</a>
</li>
<li>
    <span class="authors">Stefano Berardi and Silvia Steila</span>
    <span class="title">Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.64">10.4230/LIPIcs.TYPES.2013.64</a>
</li>
<li>
    <span class="authors">Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods</span>
    <span class="title">Extracting Imperative Programs from Proofs: In-place Quicksort</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.84">10.4230/LIPIcs.TYPES.2013.84</a>
</li>
<li>
    <span class="authors">Marc Bezem, Thierry Coquand, and Simon Huber</span>
    <span class="title">A Model of Type Theory in Cubical Sets</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.107">10.4230/LIPIcs.TYPES.2013.107</a>
</li>
<li>
    <span class="authors">Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi</span>
    <span class="title">Isomorphism of &quot;Functional&quot; Intersection Types</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.129">10.4230/LIPIcs.TYPES.2013.129</a>
</li>
<li>
    <span class="authors">Joëlle Despeyroux and Kaustuv Chaudhuri</span>
    <span class="title">A Hybrid Linear Logic for Constrained Transition Systems</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.150">10.4230/LIPIcs.TYPES.2013.150</a>
</li>
<li>
    <span class="authors">Hugo Herbelin and Arnaud Spiwack</span>
    <span class="title">The Rooster and the Syntactic Bracket</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.169">10.4230/LIPIcs.TYPES.2013.169</a>
</li>
<li>
    <span class="authors">Danko Ilik and Keiko Nakata</span>
    <span class="title">A Direct Version of Veldman&#039;s Proof of Open Induction on Cantor Space via Delimited Control Operators</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.188">10.4230/LIPIcs.TYPES.2013.188</a>
</li>
<li>
    <span class="authors">Christian Retoré</span>
    <span class="title">The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.202">10.4230/LIPIcs.TYPES.2013.202</a>
</li>
<li>
    <span class="authors">Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano</span>
    <span class="title">A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.230">10.4230/LIPIcs.TYPES.2013.230</a>
</li>
<li>
    <span class="authors">Tao Xue</span>
    <span class="title">Definitional Extension in Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2013.251">10.4230/LIPIcs.TYPES.2013.251</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