TLCA 2015 July 1-3, 2015 - Warsaw, Poland

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)



Thorsten Altenkirch (Ed.)
ISBN 978-3-939897-87-3, LIPICS Vol. 38 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 11 MB)
Search Publication Server


Authors
  • Abel, Andreas
  • Afshari, Bahareh
  • Ahrens, Benedikt
  • Altenkirch, Thorsten
  • Assaf, Ali
  • Atkey, Robert
  • Bagnol, Marc
  • Bessai, Jan
  • Bezem, Marc
  • Biernacki, Dariusz
  • Bucciarelli, Antonio
  • Capriotti, Paolo
  • Castellan, Simon
  • Chaudhuri, Kaustuv
  • Chen, Tzu-Chun
  • Clairambault, Pierre
  • Coquand, Thierry
  • Düdder, Boris
  • de’Liguoro, Ugo
  • Dudenhefner, Andrej
  • Dybjer, Peter
  • Espírito Santo, José
  • Fairweather, Elliot
  • Fernández, Maribel
  • Frey, Jonas
  • Ghani, Neil
  • Guerrieri, Giulio
  • Hötzel Escardó, Martín
  • Hetzl, Stefan
  • Hirschowitz, André
  • Hirschowitz, Tom
  • Hofmann, Martin
  • Jouannaud, Jean-Pierre
  • Kesner, Delia
  • Leigh, Graham E.
  • Li, Jianqi
  • Moser, Georg
  • Nordvall Forsberg, Fredrik
  • Paolini, Luca
  • Parmann, Erik
  • Pientka, Brigitte
  • Polesiuk, Piotr
  • Redmond, Brian F.
  • Rehof, Jakob
  • Revell, Timothy
  • Riba, Colin
  • Ronchi Della Rocca, Simona
  • Scherer, Gabriel
  • Spadotti, Régis
  • Staton, Sam
  • Szasz, Nora
  • Tabareau, Nicolas
  • Tasistro, Alvaro
  • Wang, Yuting
  • Xu, Chuangjie

  •   
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Altenkirch, Thorsten

    Abstract | Document (309 KB) | BibTeX

    Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
    Authors: Afshari, Bahareh ; Hetzl, Stefan ; Leigh, Graham E.

    Abstract | Document (527 KB) | BibTeX

    Non-Wellfounded Trees in Homotopy Type Theory
    Authors: Ahrens, Benedikt ; Capriotti, Paolo ; Spadotti, Régis

    Abstract | Document (550 KB) | BibTeX

    Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting
    Authors: Assaf, Ali

    Abstract | Document (457 KB) | BibTeX

    Models for Polymorphism over Physical Dimension
    Authors: Atkey, Robert ; Ghani, Neil ; Nordvall Forsberg, Fredrik ; Revell, Timothy ; Staton, Sam

    Abstract | Document (446 KB) | BibTeX

    MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams
    Authors: Bagnol, Marc

    Abstract | Document (621 KB) | BibTeX

    Mixin Composition Synthesis Based on Intersection Types
    Authors: Bessai, Jan ; Dudenhefner, Andrej ; Düdder, Boris ; Chen, Tzu-Chun ; de’Liguoro, Ugo ; Rehof, Jakob

    Abstract | Document (617 KB) | BibTeX

    Non-Constructivity in Kan Simplicial Sets
    Authors: Bezem, Marc ; Coquand, Thierry ; Parmann, Erik

    Abstract | Document (501 KB) | BibTeX

    Logical Relations for Coherence of Effect Subtyping
    Authors: Biernacki, Dariusz ; Polesiuk, Piotr

    Abstract | Document (508 KB) | BibTeX

    Observability for Pair Pattern Calculi
    Authors: Bucciarelli, Antonio ; Kesner, Delia ; Ronchi Della Rocca, Simona

    Abstract | Document (527 KB) | BibTeX

    Undecidability of Equality in the Free Locally Cartesian Closed Category
    Authors: Castellan, Simon ; Clairambault, Pierre ; Dybjer, Peter

    Abstract | Document (469 KB) | BibTeX

    The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation
    Authors: Hötzel Escardó, Martín ; Xu, Chuangjie

    Abstract | Document (345 KB) | BibTeX

    Curry-Howard for Sequent Calculus at Last!
    Authors: Espírito Santo, José

    Abstract | Document (465 KB) | BibTeX

    Dependent Types for Nominal Terms with Atom Substitutions
    Authors: Fairweather, Elliot ; Fernández, Maribel ; Szasz, Nora ; Tasistro, Alvaro

    Abstract | Document (455 KB) | BibTeX

    Realizability Toposes from Specifications
    Authors: Frey, Jonas

    Abstract | Document (544 KB) | BibTeX

    Standardization of a Call-By-Value Lambda-Calculus
    Authors: Guerrieri, Giulio ; Paolini, Luca ; Ronchi Della Rocca, Simona

    Abstract | Document (560 KB) | BibTeX

    Wild omega-Categories for the Homotopy Hypothesis in Type Theory
    Authors: Hirschowitz, André ; Hirschowitz, Tom ; Tabareau, Nicolas

    Abstract | Document (500 KB) | BibTeX

    Multivariate Amortised Resource Analysis for Term Rewrite Systems
    Authors: Hofmann, Martin ; Moser, Georg

    Abstract | Document (556 KB) | BibTeX

    Termination of Dependently Typed Rewrite Rules
    Authors: Jouannaud, Jean-Pierre ; Li, Jianqi

    Abstract | Document (529 KB) | BibTeX

    Well-Founded Recursion over Contextual Objects
    Authors: Pientka, Brigitte ; Abel, Andreas

    Abstract | Document (535 KB) | BibTeX

    Polynomial Time in the Parametric Lambda Calculus
    Authors: Redmond, Brian F.

    Abstract | Document (474 KB) | BibTeX

    Fibrations of Tree Automata
    Authors: Riba, Colin

    Abstract | Document (560 KB) | BibTeX

    Multi-Focusing on Extensional Rewriting with Sums
    Authors: Scherer, Gabriel

    Abstract | Document (473 KB) | BibTeX

    A Proof-theoretic Characterization of Independence in Type Theory
    Authors: Wang, Yuting ; Chaudhuri, Kaustuv

    Abstract | Document (602 KB) | BibTeX

      




    DROPS-Home | Fulltext Search | Imprint Published by LZI