Typed Lambda Calculi and Applications

1. Front Matter

   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

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

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

  Pierre-Louis Curien

Policies and ethics