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

                     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/


			PROGRAMME (ver. 31 March 2005)

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

Thursday, 21st April

08:30-09:00	Registration

09:00-10:00	
	Amy Felty (invited speaker, joint with RTA)
	A Tutorial Example of the Semantic Approach to
	Foundational Proof-Carrying Code

10:00-10:30	Tea Break

10:30-11:00	
	Olivier Hermant
	Semantic Cut Elimination in the Intuitionistic Sequent Calculus 
11:00-11:30	
	Rene David and Karim Nour
	Arithmetical Proofs of Strong Normalization Results 
	for the Symmetric Lambda-mu-calculus
11:30-12:00	
	Francois Lamarche and Lutz Strassburger 
	Naming Proofs in Classical Propositional Logic
12:00-12:30
	Francois-Regis Sinot
	Call-by-Name and Call-by-Value as Token-Passing Interaction Nets

12:30-14:00	Lunch

14:00-14:30
	Andreas Abel and Thierry Coquand
	Untyped Algorithmic Equality for Martin-Lof's Logical Framework 
	with Surjective Pairs
14:30-15:00
	Hugo Herbelin 
	On the Degeneracy of Sigma-Types 
	in Presence of Computational Classical Logic
15:00-15:30
	Ken-etsu Fujita
    	Galois Embedding from Polymorphic Types into Existential Types

15:30-17:00	Social Event (Guided City Walk)

17:30-20:30	Drink, Entertainments, Conference Dinner

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

Friday, 22nd April

09:00-10:00	
	Susumu Hayashi (invited speaker)
	Can Proofs be Animated by Games?

10:00-10:30	Tea Break

10:30-11:00	
	Carsten Schurmann, Adam Poswolsky and Jeffrey Sarnat
	The $\nabla$-Calculus. Functional Programming with Higher-Order 
	Encodings
11:00-11:30
	Christian Urban and James Cheney 
    	Avoiding Equivariance in Alpha-Prolog 
11:30-12:00
	Peter Selinger and Benoit Valiron 
    	A Lambda-calculus for Quantum Computation with Classical Control
12:00-12:30
	Greg Morrisett, Amal Ahmed, Matthew Fluet 
	L^3: A Linear Language with Locations 

12:30-14:00	Lunch

14:00-14:30
	John Power and Miki Tanaka 
	Binding Signatures for Generic Contexts
14:30-15:00
	Sam Lindley and Ian Stark
	Reducibility and TT-lifting for Computation Types
15:00-15:30
	Nick Benton and Benjamin Leperchey 
	Relational Reasoning in a Nominal Semantics for Storage

15:30-16:00	Coffee Break

16:00-16:30
	Paolo Coppola, Ugo Dal Lago and Simona Ronchi Della Rocca 
    	Elementary Affine Logic and the Call-by-Value Lambda Calculus
16:30-17:00
	Patrick Baillot and Kazushige Terui
    	A Feasible Algorithm for Typing in Elementary Affine Logic
17:00-17:30
	Ferruccio Damiani
	Rank-2 Intersection and Polymorphic Recursion

17:40-18:30	Business Meeting

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

Saturday, 23rd April

09:00-10:00	
	Thierry Coquand (invited speaker)
	Completeness Theorems and $\lambda$-calculus

10:00-10:30	Tea Break

10:30-11:00	
	Yves Bertot 
    	Filters on CoInductive Streams, an Application to Eratosthenes' Sieve
11:00-11:30
	Virgile Prevosto and Sylvain Boulme 
	Proof Contexts with Late Binding
11:30-12:00
	Stan Matwin, Amy Felty, Istvan Hernadvolgyi, and Venanzio Capretta 
    	Privacy in Data Mining Using Formal Methods
12:00-12:30
	Damiano Zanardini 
    	Higher-Order Abstract Non-Interference

12:30-14:00	Lunch

14:00-14:30
	Klaus Aehlig, Jolie G. de Miranda and C.-H. Luke Ong 
	The Monadic Second Order Theory of Trees Given by Arbitrary 
	Level Two Recursion Schemes Is Decidable 
14:30-15:00
	Paula Severi and Fer-Jan de Vries 
    	Continuity and Discontinuity in Lambda Calculus
15:00-15:30
	Jim Laird
    	The Elimination of Nesting in SPCF

15:30-16:00	Coffee Break

16:00-16:30
	Ana Bove and Venanzio Capretta 
	Recursive Functions with Higher Order Domains 
16:30-17:00
	Gilles Barthe, Benjamin Gregoire and Fernando Pastawski 
	Practical Inference for Typed-Based Termination in a 
	Polymorphic Setting
17:00-17:30
	Roberto Di Cosmo, Francois Pottie and Didier Remy 
	Subtyping Recursive Types Modulo Associative Commutative Products

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