7. TLCA 2005:
Nara, Japan
Pawel Urzyczyn (Ed.):
Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings.
Lecture Notes in Computer Science 3461 Springer 2005, ISBN 3-540-25593-1 
- 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:
L3: 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
Last update Tue May 21 00:57:25 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
