[TYPES] TLCA 2005 Call for Participation

[Hasegawa Masahito]

=======================================================================

				   TLCA 2005

			Seventh International Conference on 

                       Typed Lambda Calculi and Applications

			   21-23 April 2005, Nara, Japan

		    http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/

			   CALL FOR PARTICIPATION      

		** Early Registration Deadline: 31 March 2005 **

=======================================================================

The TLCA series of conferences serves as a forum for presenting
original research results that are broadly relevant to the theory and
applications of typed lambda calculi and related systems. This 7th
TLCA Conference will consist of 3 invited talks and 27 refereed talks.
(see the programme below).

TLCA'05 will be held as part of the Federated Conference on Rewriting,
Deduction and Programming (RDP'05), jointly with the 16th
International Conference on Rewriting Techniques and Applications
(RTA'05) and several workshops.   

Now the registration and hotel booking procedures for RDP'05 are open;
please follow the link to the registration page from the RDP'05 top
page 

	http://www.kurims.kyoto-u.ac.jp/rdp05/

to complete your registration. There also are links to web pages
providing some travel and local information. 

Please remember that the number of hotel rooms is limited. Requests
will be processed on a first come first served basis and will be
subject to availability.

RDP'05 will take place at the Nara-Ken New Public Hall which is
located in the centre of the beautiful Nara National Park, within 20
minutes walk from the Kintestu Nara Station. 

CONTACT

 Enquiries regarding the registration and hotel booking should be sent
 to the RDP'05 organizers <rdp05 at m.aist.go.jp>. Enquiries regarding
 the TLCA conference should be sent to the TLCA'05 organizers
 <tlca05org at kurims.kyoto-u.ac.jp>.

FURTHER INFORMATION

 RDP'05 website:	http://www.kurims.kyoto-u.ac.jp/rdp05/
 TLCA'05 website:	http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/

=======================================================================

PROGRAMME of TLCA 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-22: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, 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 Linear Logics 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:30-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 Co-Inductive 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, 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, Fernando Pastawski 
	Practical Inference for Typed-based Termination in a 
	Polymorphic Setting
17:00-17:30
	Roberto Di Cosmo, Francois Pottier, Didier Remy 
	Subtyping Recursive Types Modulo Associative Commutative Products

=======================================================================