HTML Export for TYPES 2021

Copy to Clipboard Download

<h2>LIPIcs, Volume 239, TYPES 2021</h2>
<ul>
<li>
    <span class="authors">Henning Basold, Jesper Cockx, and Silvia Ghilezan</span>
    <span class="title">LIPIcs, Volume 239, TYPES 2021, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021">10.4230/LIPIcs.TYPES.2021</a>
</li>
<li>
    <span class="authors">Henning Basold, Jesper Cockx, and Silvia Ghilezan</span>
    <span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.0">10.4230/LIPIcs.TYPES.2021.0</a>
</li>
<li>
    <span class="authors">Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer</span>
    <span class="title">Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.1">10.4230/LIPIcs.TYPES.2021.1</a>
</li>
<li>
    <span class="authors">Thibaut Benjamin</span>
    <span class="title">Formalisation of Dependent Type Theory: The Example of CaTT</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.2">10.4230/LIPIcs.TYPES.2021.2</a>
</li>
<li>
    <span class="authors">Rafaël Bocquet</span>
    <span class="title">Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.3">10.4230/LIPIcs.TYPES.2021.3</a>
</li>
<li>
    <span class="authors">William DeMeo and Jacques Carette</span>
    <span class="title">A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.4">10.4230/LIPIcs.TYPES.2021.4</a>
</li>
<li>
    <span class="authors">Pietro Di Gianantonio and Marina Lenisa</span>
    <span class="title">Principal Types as Lambda Nets</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.5">10.4230/LIPIcs.TYPES.2021.5</a>
</li>
<li>
    <span class="authors">István Donkó and Ambrus Kaposi</span>
    <span class="title">Internal Strict Propositions Using Point-Free Equations</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.6">10.4230/LIPIcs.TYPES.2021.6</a>
</li>
<li>
    <span class="authors">Giulio Fellin, Sara Negri, and Eugenio Orlandelli</span>
    <span class="title">Constructive Cut Elimination in Geometric Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.7">10.4230/LIPIcs.TYPES.2021.7</a>
</li>
<li>
    <span class="authors">Asta Halkjær From</span>
    <span class="title">A Succinct Formalization of the Completeness of First-Order Logic</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.8">10.4230/LIPIcs.TYPES.2021.8</a>
</li>
<li>
    <span class="authors">Christa Jenkins, Andrew Marmaduke, and Aaron Stump</span>
    <span class="title">Simulating Large Eliminations in Cedille</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.9">10.4230/LIPIcs.TYPES.2021.9</a>
</li>
<li>
    <span class="authors">Georgi Nakov and Fredrik Nordvall Forsberg</span>
    <span class="title">Quantitative Polynomial Functors</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.10">10.4230/LIPIcs.TYPES.2021.10</a>
</li>
<li>
    <span class="authors">Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez</span>
    <span class="title">Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.11">10.4230/LIPIcs.TYPES.2021.11</a>
</li>
<li>
    <span class="authors">Yuta Takahashi</span>
    <span class="title">Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2021.12">10.4230/LIPIcs.TYPES.2021.12</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