Skip to main content
SpringerLink
Log in

Typed Lambda Calculi and Applications

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

  • Conference proceedings
  • © 2009

Overview

Editors:
  1. Pierre-Louis Curien

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: TLCA 2009.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (29 papers)

  1. Front Matter

    Download chapter PDF

  2. Mathematical Synthesis of Equational Deduction Systems

    • Marcelo Fiore, Chung-Kil Hur
    Pages 1-2

  3. A Pronominal Approach to Binding and Computation

    • Robert Harper, Daniel R. Licata, Noam Zeilberger
    Pages 3-4

  4. A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

    • Andreas Abel, Thierry Coquand, Miguel Pagano
    Pages 5-19

  5. Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1

    • Federico Aschieri, Stefano Berardi
    Pages 20-34

  6. Syntax for Free: Representing Syntax with Binding Using Parametricity

    • Robert Atkey
    Pages 35-49

  7. On the Meaning of Logical Completeness

    • Michele Basaldella, Kazushige Terui
    Pages 50-64

  8. Thick Subtrees, Games and Experiments

    • Pierre Boudes
    Pages 65-79

  9. Bounded Linear Logic, Revisited

    • Ugo Dal Lago, Martin Hofmann
    Pages 80-94

  10. Partial Orders, Event Structures and Linear Strategies

    • Claudia Faggian, Mauro Piccolo
    Pages 95-111

  11. Existential Type Systems with No Types in Terms

    • Ken-etsu Fujita, Aleksy Schubert
    Pages 112-126

  12. Initial Algebra Semantics for Cyclic Sharing Structures

    • Makoto Hamana
    Pages 127-141

  13. An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form

    • Hugo Herbelin, Stéphane Zimmermann
    Pages 142-156

  14. Refinement Types as Proof Irrelevance

    • William Lovas, Frank Pfenning
    Pages 157-171

  15. Weak ω-Categories from Intensional Type Theory

    • Peter LeFanu Lumsdaine
    Pages 172-187

  16. Relating Classical Realizability and Negative Translation for Existential Witness Extraction

    • Alexandre Miquel
    Pages 188-202

  17. Session-Based Communication Optimisation for Higher-Order Mobile Processes

    • Dimitris Mostrous, Nobuko Yoshida
    Pages 203-218

  18. The Cut-Elimination Theorem for Differential Nets with Promotion

    • Michele Pagani
    Pages 219-233

  19. A Polymorphic Type System for the Lambda-Calculus with Constructors

    • Barbara Petit
    Pages 234-248

  20. Kripke Semantics for Martin-Löf’s Extensional Type Theory

    • Steve Awodey, Florian Rabe
    Pages 249-263
Back to top

Other volumes

  1. Typed Lambda Calculi and Applications

Keywords

About this book

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.

Editors and Affiliations

  • Laboratoire PPS (CNRS / Paris 7), Case 7014, Université Paris Diderot - Paris 7, Paris Cedex 13, France

    Pierre-Louis Curien

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation