TYPES 2022 June 20-25, 2022, LS2N, University of Nantes, France

28th International Conference on Types for Proofs and Programs (TYPES 2022)



Delia Kesner and Pierre-Marie Pédrot (Eds.)
ISBN 978-3-95977-285-3, LIPICS Vol. 269 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 4 MB)
Search Publication Server

Authors
  • Ahrens, Benedikt
  • Altenkirch, Thorsten
  • Alves, Sandra
  • Bezem, Marc
  • Birkedal, Lars
  • Blot, Valentin
  • Bradley, Felix
  • Colledan, Andrea
  • Coquand, Thierry
  • Dal Lago, Ugo
  • Dubois, Catherine
  • Dybjer, Peter
  • Escardó, Martín
  • Florido, Mário
  • Geuvers, Herman
  • Giorgetti, Alain
  • Gratzer, Daniel
  • Grienenberger, Emilie
  • Hurkens, Tonny
  • Kaposi, Ambrus
  • Kesner, Delia
  • Ledein, Amélie
  • Luo, Zhaohui
  • Magaud, Nicolas
  • Matthes, Ralph
  • Mull, Nathan
  • Mulligan, Dominic P.
  • Mörtberg, Anders
  • Padovani, Luca
  • Pédrot, Pierre-Marie
  • Reis, Fábio
  • Stassen, Philipp
  • Végh, Tamás
  • Wullaert, Kobe
  • Zeuner, Max
  • Šinkarovs, Artjoms
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Kesner, Delia ; Pédrot, Pierre-Marie

    Abstract | Document (489 KB) | BibTeX

    All Watched Over by Machines of Loving Grace
    Authors: Mulligan, Dominic P.

    Abstract | Document (796 KB) | BibTeX

    Classical Natural Deduction from Truth Tables
    Authors: Geuvers, Herman ; Hurkens, Tonny

    Abstract | Document (779 KB) | BibTeX

    On Dynamic Lifting and Effect Typing in Circuit Description Languages
    Authors: Colledan, Andrea ; Dal Lago, Ugo

    Abstract | Document (852 KB) | BibTeX

    Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory
    Authors: Grienenberger, Emilie

    Abstract | Document (974 KB) | BibTeX

    On the Fair Termination of Client-Server Sessions
    Authors: Padovani, Luca

    Abstract | Document (849 KB) | BibTeX

    {mitten}: A Flexible Multimodal Proof Assistant
    Authors: Stassen, Philipp ; Gratzer, Daniel ; Birkedal, Lars

    Abstract | Document (939 KB) | BibTeX

    An Irrelevancy-Eliminating Translation of Pure Type Systems
    Authors: Mull, Nathan

    Abstract | Document (746 KB) | BibTeX

    Linear Rank Intersection Types
    Authors: Reis, Fábio ; Alves, Sandra ; Florido, Mário

    Abstract | Document (781 KB) | BibTeX

    A Metatheoretic Analysis of Subtype Universes
    Authors: Bradley, Felix ; Luo, Zhaohui

    Abstract | Document (812 KB) | BibTeX

    The Münchhausen Method in Type Theory
    Authors: Altenkirch, Thorsten ; Kaposi, Ambrus ; Šinkarovs, Artjoms ; Végh, Tamás

    Abstract | Document (703 KB) | BibTeX

    Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families
    Authors: Dubois, Catherine ; Magaud, Nicolas ; Giorgetti, Alain

    Abstract | Document (685 KB) | BibTeX

    A Semantics of 𝕂 into Dedukti
    Authors: Ledein, Amélie ; Blot, Valentin ; Dubois, Catherine

    Abstract | Document (1,059 KB) | BibTeX

    Type Theory with Explicit Universe Polymorphism
    Authors: Bezem, Marc ; Coquand, Thierry ; Dybjer, Peter ; Escardó, Martín

    Abstract | Document (758 KB) | BibTeX

    A Univalent Formalization of Constructive Affine Schemes
    Authors: Zeuner, Max ; Mörtberg, Anders

    Abstract | Document (953 KB) | BibTeX

    Univalent Monoidal Categories
    Authors: Wullaert, Kobe ; Matthes, Ralph ; Ahrens, Benedikt

    Abstract | Document (954 KB) | BibTeX

    		  



    DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI