Theoretical Aspects of Computer Software

Invited Talk 1.- A Spatial Logic for Concurrency (Part I).- Session 1.- Boxed Ambients.- A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation.- Formal Eavesdropping and Its Computational Interpretation.- Invited Talk 2.- Resource-Passing Concurrent Programming.- Session 2.- Solo Diagrams.- Observational Equivalence for Synchronized Graph Rewriting with Mobility.- Session 3.- Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness.- Termination Proofs and Complexity Certification.- A Renee Equation for Algorithmic Complexity.- Invited Talk 3.- Nominal Logic: A First Order Theory of Names and Binding.- Session 4.- A Logic Programming Language Based on Binding Algebras.- Proof-Search and Countermodel Generation in Propositional BI Logic.- Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders.- Invited Talk 4.- Modelisation of Timed Automata in Coq.- Session 5.- Model-Checking LTL with Regular Valuations for Pushdown Systems.- What Will Be Eventually True of Polynomial Hybrid Automata?.- Non-structural Subtype Entailment in Automata Theory.- Session 6.- Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems.- Weakest Congruence Results Concerning "Any-Lock".- Invited Talk 5.- Design and Correctness of Program Transformations Based on Control-Flow Analysis.- Session 7.- Infinite Intersection and Union Types for the Lazy Lambda Calculus.- Strong Normalization of Second Order Symmetric Lambda-mu Calculus.- The Girard-Reynolds Isomorphism.- Invited Talk 6.- Lightweight Analysis of Object Interactions.- Session 8.- Typing Assembly Programs with Explicit Forwarding.- The UDP Calculus: Rigorous Semantics for Real Networking.- TACS Open Lecture.- Unison: A File Synchronizer and Its Specification.