HTML Export for TYPES 2022

Copy to Clipboard Download

<h2>LIPIcs, Volume 269, TYPES 2022</h2>
<ul>
<li>
    <span class="authors">Delia Kesner and Pierre-Marie Pédrot</span>
    <span class="title">LIPIcs, Volume 269, TYPES 2022, Complete Volume</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022">10.4230/LIPIcs.TYPES.2022</a>
</li>
<li>
    <span class="authors">Delia Kesner and Pierre-Marie Pédrot</span>
    <span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.0">10.4230/LIPIcs.TYPES.2022.0</a>
</li>
<li>
    <span class="authors">Dominic P. Mulligan</span>
    <span class="title">All Watched Over by Machines of Loving Grace</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.1">10.4230/LIPIcs.TYPES.2022.1</a>
</li>
<li>
    <span class="authors">Herman Geuvers and Tonny Hurkens</span>
    <span class="title">Classical Natural Deduction from Truth Tables</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.2">10.4230/LIPIcs.TYPES.2022.2</a>
</li>
<li>
    <span class="authors">Andrea Colledan and Ugo Dal Lago</span>
    <span class="title">On Dynamic Lifting and Effect Typing in Circuit Description Languages</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.3">10.4230/LIPIcs.TYPES.2022.3</a>
</li>
<li>
    <span class="authors">Emilie Grienenberger</span>
    <span class="title">Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.4">10.4230/LIPIcs.TYPES.2022.4</a>
</li>
<li>
    <span class="authors">Luca Padovani</span>
    <span class="title">On the Fair Termination of Client-Server Sessions</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.5">10.4230/LIPIcs.TYPES.2022.5</a>
</li>
<li>
    <span class="authors">Philipp Stassen, Daniel Gratzer, and Lars Birkedal</span>
    <span class="title">{mitten}: A Flexible Multimodal Proof Assistant</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.6">10.4230/LIPIcs.TYPES.2022.6</a>
</li>
<li>
    <span class="authors">Nathan Mull</span>
    <span class="title">An Irrelevancy-Eliminating Translation of Pure Type Systems</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.7">10.4230/LIPIcs.TYPES.2022.7</a>
</li>
<li>
    <span class="authors">Fábio Reis, Sandra Alves, and Mário Florido</span>
    <span class="title">Linear Rank Intersection Types</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.8">10.4230/LIPIcs.TYPES.2022.8</a>
</li>
<li>
    <span class="authors">Felix Bradley and Zhaohui Luo</span>
    <span class="title">A Metatheoretic Analysis of Subtype Universes</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.9">10.4230/LIPIcs.TYPES.2022.9</a>
</li>
<li>
    <span class="authors">Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh</span>
    <span class="title">The Münchhausen Method in Type Theory</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.10">10.4230/LIPIcs.TYPES.2022.10</a>
</li>
<li>
    <span class="authors">Catherine Dubois, Nicolas Magaud, and Alain Giorgetti</span>
    <span class="title">Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.11">10.4230/LIPIcs.TYPES.2022.11</a>
</li>
<li>
    <span class="authors">Amélie Ledein, Valentin Blot, and Catherine Dubois</span>
    <span class="title">A Semantics of 𝕂 into Dedukti</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.12">10.4230/LIPIcs.TYPES.2022.12</a>
</li>
<li>
    <span class="authors">Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó</span>
    <span class="title">Type Theory with Explicit Universe Polymorphism</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.13">10.4230/LIPIcs.TYPES.2022.13</a>
</li>
<li>
    <span class="authors">Max Zeuner and Anders Mörtberg</span>
    <span class="title">A Univalent Formalization of Constructive Affine Schemes</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.14">10.4230/LIPIcs.TYPES.2022.14</a>
</li>
<li>
    <span class="authors">Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens</span>
    <span class="title">Univalent Monoidal Categories</span>
    <a class="doi" href="https://doi.org/10.4230/LIPIcs.TYPES.2022.15">10.4230/LIPIcs.TYPES.2022.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