Typed Lambda Calculi and Applications

1. Front Matter

   PDF

2. Completeness Theorems and λ-Calculus

   1. Completeness Theorems and λ-Calculus

      • Thierry Coquand

      Pages 1-9

   2. A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract

      • Amy P. Felty

      Pages 10-10

   3. Can Proofs Be Animated By Games?

      • Susumu Hayashi

      Pages 11-22

3. Contributed Papers

   1. Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs

      • Andreas Abel, Thierry Coquand

      Pages 23-38

   2. The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable

      • Klaus Aehlig, Jolie G. de Miranda, C. -H. Luke Ong

      Pages 39-54

   3. A Feasible Algorithm for Typing in Elementary Affine Logic

      • Patrick Baillot, Kazushige Terui

      Pages 55-70

   4. Practical Inference for Type-Based Termination in a Polymorphic Setting

      • Gilles Barthe, Benjamin Grégoire, Fernando Pastawski

      Pages 71-85

   5. Relational Reasoning in a Nominal Semantics for Storage

      • Nick Benton, Benjamin Leperchey

      Pages 86-101

   6. Filters on CoInductive Streams, an Application to Eratosthenes’ Sieve

      • Yves Bertot

      Pages 102-115

   7. Recursive Functions with Higher Order Domains

      • Ana Bove, Venanzio Capretta

      Pages 116-130

   8. Elementary Affine Logic and the Call-by-Value Lambda Calculus

      • Paolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca

      Pages 131-145

   9. Rank-2 Intersection and Polymorphic Recursion

      • Ferruccio Damiani

      Pages 146-161

   10. Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus

       • René David, Karim Nour

       Pages 162-178

   11. Subtyping Recursive Types Modulo Associative Commutative Products

       • Roberto Di Cosmo, François Pottier, Didier Rémy

       Pages 179-193

   12. Galois Embedding from Polymorphic Types into Existential Types

       • Ken-etsu Fujita

       Pages 194-208

   13. On the Degeneracy of Σ-Types in Presence of Computational Classical Logic

       • Hugo Herbelin

       Pages 209-220

   14. Semantic Cut Elimination in the Intuitionistic Sequent Calculus

       • Olivier Hermant

       Pages 221-233

   15. The Elimination of Nesting in SPCF

       • J. Laird

       Pages 234-245

   16. Naming Proofs in Classical Propositional Logic

       • François Lamarche, Lutz Straßburger

       Pages 246-261

The 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005) was held in Nara (Japan) from 21 to 23 April 2005, as part of the Joint Conference on Rewriting, Deduction and Programming (RDP 2005). This book contains the contributed papers, and extended abstracts of two invited talks, given by Thierry Coquand and Susumu Hayashi. A short abstract of the joint RDP invited lecture by Amy Felty is also included. The 27 contributed papers were selected from 61 submissions of generally very high quality, and the Program Committee had a hard time making the selection. The editor would like to thank everyone who submitted a paper and to express his regret that many interesting works could not be included. The editor also wishes to thank the invited speakers, the members of the Program and Organizing Committees, the Publicity Chair, and the referees for their joint e?ort towards the success of the conference. The support from the Nara Convention Bureau is gratefully acknowledged. The typed lambda calculus continues to be an important tool in logic and theoretical computer science. Since 1993, the research progress in this area has been documented by the TLCA proceedings. The present volume contributes to this tradition.

• Signatur
• algorithm
• algorithms
• computational logic
• formal method
• formal methods
• lambda calculus
• logic
• logical relations
• program semantics
• programming
• programming calculi
• programming theory
• semantics
• type systems

• Institute of Informatics, University of Warsaw, Poland

  Paweł Urzyczyn

Policies and ethics