7. TLCA 2005: Nara, Japan

• Thierry Coquand:
  Completeness Theorems and lambda-Calculus. 1-9
  
• Amy P. Felty:
  A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract. 10-10
  
• Susumu Hayashi:
  Can Proofs Be Animated By Games? 11-22
  

Contributed Papers

• Andreas Abel, Thierry Coquand:
  Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. 23-38
  
• Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong:
  The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. 39-54
  
• Patrick Baillot, Kazushige Terui:
  A Feasible Algorithm for Typing in Elementary Affine Logic. 55-70
  
• Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
  Practical Inference for Type-Based Termination in a Polymorphic Setting. 71-85
  
• Nick Benton, Benjamin Leperchey:
  Relational Reasoning in a Nominal Semantics for Storage. 86-101
  
• Yves Bertot:
  Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. 102-115
  
• Ana Bove, Venanzio Capretta:
  Recursive Functions with Higher Order Domains. 116-130
  
• Paolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca:
  Elementary Affine Logic and the Call-by-Value Lambda Calculus. 131-145
  
• Ferruccio Damiani:
  Rank-2 Intersection and Polymorphic Recursion. 146-161
  
• René David, Karim Nour:
  Arithmetical Proofs of Strong Normalization Results for the Symmetric lambda-µ-Calculus. 162-178
  
• Roberto Di Cosmo, François Pottier, Didier Rémy:
  Subtyping Recursive Types Modulo Associative Commutative Products. 179-193
  
• Ken-etsu Fujita:
  Galois Embedding from Polymorphic Types into Existential Types. 194-208
  
• Hugo Herbelin:
  On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. 209-220
  
• Olivier Hermant:
  Semantic Cut Elimination in the Intuitionistic Sequent Calculus. 221-233
  
• James Laird:
  The Elimination of Nesting in SPCF. 234-245
  
• François Lamarche, Lutz Straßburger:
  Naming Proofs in Classical Propositional Logic. 246-261
  
• Sam Lindley, Ian Stark:
  Reducibility and TT-Lifting for Computation Types. 262-277
  
• Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta:
  Privacy in Data Mining Using Formal Methods. 278-292
  
• Greg Morrisett, Amal J. Ahmed, Matthew Fluet:
  L³: A Linear Language with Locations. 293-307
  
• John Power, Miki Tanaka:
  Binding Signatures for Generic Contexts. 308-323
  
• Virgile Prevosto, Sylvain Boulmé:
  Proof Contexts with Late Binding. 324-338
  
• Carsten Schürmann, Adam Poswolsky, Jeffrey Sarnat:
  The [triangle]-Calculus. Functional Programming with Higher-Order Encodings. 339-353
  
• Peter Selinger, Benoît Valiron:
  A Lambda Calculus for Quantum Computation with Classical Control. 354-368
  
• Paula Severi, Fer-Jan de Vries:
  Continuity and Discontinuity in Lambda Calculus. 369-385
  
• François-Régis Sinot:
  Call-by-Name and Call-by-Value as Token-Passing Interaction Nets. 386-400
  
• Christian Urban, James Cheney:
  Avoiding Equivariance in Alpha-Prolog. 401-416
  
• Damiano Zanardini:
  Higher-Order Abstract Non-interference. 417-432