======================================================================= 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@m.aist.go.jp>. Enquiries regarding the TLCA conference should be sent to the TLCA'05 organizers <tlca05org@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 =======================================================================