TYPES 2019 June 11-14, 2019, Oslo, Norway

25th International Conference on Types for Proofs and Programs (TYPES 2019)



Marc Bezem and Assia Mahboubi (Eds.)
ISBN 978-3-95977-158-0, LIPICS Vol. 175 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 6 MB)
Search Publication Server

Authors
  • Altenkirch, Thorsten
  • Alves, Sandra
  • Bezem, Marc
  • Bos, Nathaniel
  • Cockx, Jesper
  • Danielsson, Nils Anders
  • Geniet, Colin
  • Kaposi, Ambrus
  • Kesner, Delia
  • Kohlhase, Michael
  • Kovács, András
  • Kraus, Nicolai
  • Kravchuk-Kirilyuk, Anastasiya
  • Lafont, Ambroise
  • Mahboubi, Assia
  • Monnier, Stefan
  • Piceghello, Stefano
  • Pinyo, Gun
  • Rabe, Florian
  • Ventura, Daniel
  • Voizard, Antoine
  • Weirich, Stephanie
  • Wenzel, Makarius
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Bezem, Marc ; Mahboubi, Assia

    Abstract | Document (307 KB) | BibTeX

    Making Isabelle Content Accessible in Knowledge Representation Formats
    Authors: Kohlhase, Michael ; Rabe, Florian ; Wenzel, Makarius

    Abstract | Document (860 KB) | BibTeX

    Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules
    Authors: Cockx, Jesper

    Abstract | Document (588 KB) | BibTeX

    A Quantitative Understanding of Pattern Matching
    Authors: Alves, Sandra ; Kesner, Delia ; Ventura, Daniel

    Abstract | Document (726 KB) | BibTeX

    Big Step Normalisation for Type Theory
    Authors: Altenkirch, Thorsten ; Geniet, Colin

    Abstract | Document (479 KB) | BibTeX

    From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
    Authors: Pinyo, Gun ; Kraus, Nicolai

    Abstract | Document (573 KB) | BibTeX

    For Finitary Induction-Induction, Induction Is Enough
    Authors: Kaposi, Ambrus ; Kovács, András ; Lafont, Ambroise

    Abstract | Document (606 KB) | BibTeX

    Eta-Equivalence in Core Dependent Haskell
    Authors: Kravchuk-Kirilyuk, Anastasiya ; Voizard, Antoine ; Weirich, Stephanie

    Abstract | Document (682 KB) | BibTeX

    Coherence for Monoidal Groupoids in HoTT
    Authors: Piceghello, Stefano

    Abstract | Document (616 KB) | BibTeX

    Is Impredicativity Implicitly Implicit?
    Authors: Monnier, Stefan ; Bos, Nathaniel

    Abstract | Document (573 KB) | BibTeX

    Higher Inductive Type Eliminators Without Paths
    Authors: Danielsson, Nils Anders

    Abstract | Document (437 KB) | BibTeX

    		  



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