Typed Lambda Calculi and Applications

9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings

  • Pierre-Louis Curien
Conference proceedings TLCA 2009

Part of the Lecture Notes in Computer Science book series (LNCS, volume 5608)

Table of contents

  1. Front Matter
  2. Marcelo Fiore, Chung-Kil Hur
    Pages 1-2
  3. Robert Harper, Daniel R. Licata, Noam Zeilberger
    Pages 3-4
  4. Michele Basaldella, Kazushige Terui
    Pages 50-64
  5. Pierre Boudes
    Pages 65-79
  6. Ugo Dal Lago, Martin Hofmann
    Pages 80-94
  7. Claudia Faggian, Mauro Piccolo
    Pages 95-111
  8. Ken-etsu Fujita, Aleksy Schubert
    Pages 112-126
  9. William Lovas, Frank Pfenning
    Pages 157-171
  10. Peter LeFanu Lumsdaine
    Pages 172-187
  11. Dimitris Mostrous, Nobuko Yoshida
    Pages 203-218
  12. Steve Awodey, Florian Rabe
    Pages 249-263
  13. Colin Riba
    Pages 264-278
  14. Jeffrey Sarnat, Carsten Schürmann
    Pages 279-293
  15. Florian Stenger, Janis Voigtländer
    Pages 294-308
  16. Christine Tasson
    Pages 325-340
  17. Takeshi Tsukada, Atsushi Igarashi
    Pages 341-355
  18. Paweł Urzyczyn
    Pages 356-370
  19. Lionel Vaux
    Pages 371-385
  20. Gunnar Wilken, Andreas Weiermann
    Pages 386-400
  21. Back Matter

About these proceedings


This book constitutes the refereed proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th International Conference on Rewriting Techniques and Applications as part of RDP 2009, the 5th International Conference on Rewriting, Deduction, and Programming.

The 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. The papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.


Cut-elimination theorem Heyting arithmetic algorithms bounded linear logic completeness complexity deduction systems games lambda calculus omega categories optimization partial orders proof proof theory type checking

Editors and affiliations

  • Pierre-Louis Curien
    • 1
  1. 1.Laboratoire PPS (CNRS / Paris 7), Case 7014Université Paris Diderot - Paris 7Paris Cedex 13France

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2009
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-642-02272-2
  • Online ISBN 978-3-642-02273-9
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
IT & Software