Wednesday Dec 10: 9:00-10:00 Session Chair: V. Saraswat, IBM TJ Watson Research Center, USA and The Pennsylvania State University, USA Plenary Invited Talk (with ICLP) by Greg Morrisett Achieving Type Safety for Low-Level Code G. Morrisett, Cornell University, USA 10:00-10:30 Coffee Break 10:30-12:30 Regular Session Chaired by: TBD Kernel Mode Linux: Towards an operating system protected by a type theory T. Maeda, University of Tokyo, JAPAN A. Yonezawa, University of Tokyo, JAPAN Self Configurable Mirror Servers for Automatic Adaptation to Service Demand Fluctuation M. Agetsuma, University of Electro-Communications, JAPAN K. Kono, University of Electro-Communications, JAPAN H. Iwasaki, University of Electro-Communications, JAPAN T. Masuda, University of Electro-Communications, JAPAN Information Flow Security for XML Transformations V. Benzaken, Universite Paris-Sud, FRANCE M. Burelle, Universite Paris-Sud, FRANCE G. Castagna, Ecole Normale Superieure, FRANCE Unreliable Failure Detectors via Operational Semantics U. Nestmann, EPFL Lausanne, SWITZERLAND R. Fuzzati, EPFL Lausanne, SWITZERLAND 12:30-14:00 Lunch 14:00-22:00 Social event ( excursion / banquet ) Thursday Dec 11 9:00-10:30 Session Chair: R. Shyamsundar, Tata Institute of Fundamental Research, India 9:00-10:00 Invited Talk by Andrew Birrell Bankable Postage for Network Servics M. Abadi, University of California, Santa Cruz, USA A. Birrell, Microsoft Research, USA M. Burrows, Google, USA F. Dabek, MIT, USA T. Wobber, Microsoft Research, USA 10:00-10:30 Regular Talk Global Predicate Detection under Fine-grained Modalities P. Chandra, University of Illinois at Chicago, USA A. Kshemkalyani, University of Illinois at Chicago, USA 10:30-11:00 CB 11:00-12:30 Regular Session Chaired by: TBD Combining Hierarchical Specification with Hierarchical Implementation N. Zhan, Mannheim University, GERMANY Automatic Generation of Simple Lemmas from Recursive Definitions using Decision Procedures D. Kapur, University of New Mexico, USA M. Subramaniam, University of Nebraska, USA Deaccumulation -- Improving Provability J. Giesl, RWTH Aachen, GERMANY A. Kuhnemann, Dresden University of Technology, GERMANY J. Voigtlander, Dresden University of Technology, GERMANY 12:30-14:00 Lunch 2:30-4:00 Regular Session Chaired by: TBD Incentive Compatible Mechanism Based on Linear Pricing Schemes for Single-Minded Auction N. Chen, Fudan University, CHINA H. Zhu, Fudan University, CHINA Hierarchical structure of 1-safe Petri nets K. Lodaya, Intitute of Mathematical Sciences, INDIA D. Ranganayakulu, SIVET College, INDIA K. Rangarajan, Madras Christian College, INDIA A Calculus for Secure Mobility B. Blanchet, Ecole Normale Superieure, France and Max-Planck-Insitute for Informatics, GERMANY B. Aziz, Dublin City University, IRELAND A Calculus of Bounded Capacities F. Barbanera, Universita di Catania, ITALY M. Bugliesi, Universita Ca Foscari, ITALY M. Dezani-Ciancaglini, Universita di Torino, ITALY V. Sassone, University of Sussex, UK 4:00-4:30 Coffee Break Friday Dec 12 9:00-10:30 Session Chair: K. Ueda, Waseda University, JAPAN 9:00-10:00 Invited Talk by Mark Miller Paradigm Regained: Abstraction Mechanisms for Access Control M. Miller, Hewlett Packard Laboratories and Johns Hopkins University, USA J. Shapiro, Johns Hopkins University, USA 10:00-10:30 Regular Talk The Design and Evaluation of a Middleware Library for Distribution of Language Entities E. Klintskog, Swedish Insitute of Computer Science, SWEDEN Z. El Banna, IMIT-Royal Institute of Technology, SWEDEN P. Brand, Swedish Insitute of Computer Science, SWEDEN S. Haridi, IMIT-Royal Institute of Technology, SWEDEN 10:30-11:00 Coffee Break 11:00-12:30 Regular Session Chaired by: TBD Generating optimal Linear Temporal Logic monitors by coinduction K. Sen, University of Illionis at Urbana-Champaign, USA G. Rosu, University of Illionis at Urbana-Champaign, USA G. Agha, University of Illionis at Urbana-Champaign, USA Probabilistic Timed Simulation Verification and its application to Stepwise Refinement of Real-Time Systems S. Yamane, Kanazawa University, JAPAN Model Checking Probabilistic Distributed Systems B. Bollig, RWTH Aachen, GERMANY M. Leucker, Uppsala University, SWEDEN END OF THE MEETING.