Papers accepted for presentation at the 
                     Seventh International Conference on
              Typed Lambda Calculi and Applications (TLCA '05)
                                  Nara, Japan
                               21-23 April 2005
                     (Colocated with RTA as RDP '05)
                  http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/


 1. Andreas Abel and Thierry Coquand
    Untyped Algorithmic Equality for Martin-Löf's Logical Framework 
    with Surjective Pairs

 2. Klaus Aehlig, Jolie G de Miranda, Luke Ong
    The Monadic Second Order Theory of Trees Given by Arbitrary Level Two 
    Recursion Schemes Is Decidable 

 3. P.Baillot, K. Terui
    A feasible algorithm for typing in Elementary Affine Logic

 4. Gilles Barthe, Benjamin Gregoire, Fernando Pastawski
    Practical inference for typed-based termination in a polymorphic setting

 5. Nick Benton and Benjamin Leperchey
    Relational Reasoning in a Nominal Semantics for Storage

 6. Yves Bertot
    Filters on Co-Inductive streams: an application to Eratosthenes' sieve

 7. Ana Bove and Venanzio Capretta
    Recursive functions with higher order domains 

 8. Paolo Coppola, Ugo Dal Lago and Simona Ronchi Della Rocca
    Elementary Linear Logics and the Call-by-value lambda calculus

 9. Ferruccio Damiani
    Rank-2 Intersection and Polymorphic Recursion

10. Rene David and Karim Nour
    Arithmetical proofs of strong normalization results 
    for the symmetric lambda-mu-calculus

11. Roberto Di Cosmo, François Pottier, Didier Rémy
    Subtyping Recursive Types modulo Associative Commutative Products

12. Ken-etsu Fujita
    Galois embedding from polymorphic types into existential types

13. Hugo Herbelin
    On the degeneracy of sigma-types 
    in presence of computational classical logic

14. Olivier Hermant
    Semantic cut elimination in the Intuitionnistic Sequent Calculus 

15. Francois Lamarche and Lutz Strassburger
    Naming Proofs in Classical Propositional Logic

16. Jim Laird
    The Elimination of Nesting in SPCF

17. Sam Lindley and Ian Stark
    Reducibility and TT-lifting for Computation Types

18. Stan Matwin, Amy Felty, Istvan Hernadvolgyi, and Venanzio Capretta
    Privacy in Data Mining Using Formal Methods

19. Greg Morrisett, Amal Ahmed, Matthew Fluet
    L^3: A Linear Language with Locations 

20. John Power and Miki Tanaka
    Binding Signatures for Generic Contexts

21. Virgile Prevosto and Sylvain Boulme
    Proof Contexts with Late Binding

22. Carsten Schurmann, Adam Poswolsky, Jeffrey Sarnat
    The $\nabla$-Calculus. Functional Programming with Higher-order Encodings

23. Peter Selinger and Benoit Valiron
    A lambda-calculus for quantum computation with classical control

24. Paula Severi and Fer-Jan de Vries
    Continuity and Discontinuity in Lambda Calculus

25. François-Régis Sinot
    Call-by-Name and Call-by-Value as Token-Passing Interaction Nets

26. Christian Urban and James Cheney
    Avoiding Equivariance in Alpha-Prolog 

27. Damiano Zanardini
    Higher-Order Abstract Non-Interference


-----------------------------------------------------------------------