CONTENTS -- Preface -- A Short Research Biography of Mario Coppo, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca -- ICTCS 2007: October 3-5 2007, Rome, Italy -- Part A Invited Talks -- Clairvoyance and Laziness for on Line Travelling Agents G. Ausiello -- Proving the Range Property for Lambda Theories and Models H. Barendregt -- Can a Proper Lambda-Model have an R.E. Equational Theory? C. Berline -- Bibliography -- Session Centered Calculi for Service Oriented Computing R. De Nicola -- 1. Introduction -- Acknowledgments -- Bibliography -- Symmetries in Foundations G. Longo -- Bibliography -- Part B Regular Contributions -- On the Approximability of Dense Steiner Tree Problems M. Hauptmann -- 1. Introduction -- 2. Exact Algorithms for the Steiner Tree Problem -- 3. The -Dense Steiner Tree Problem -- 3.1. Towards Average-Density: Relaxing the Density Condition -- 4. The Dense Steiner Forest Problem -- 5. Conclusion -- References -- Weak Pattern Matching in Colored Graphs: Minimizing the Number of Connected Components R. Dondi, G. Fertin, and S. Vialette -- 1. Introduction -- 2. Preliminaries -- 3. Hardness result for paths -- 4. Fixed-parameter algorithms -- 4.1. The MIN-CC problem is fixed-parameter tractable -- 4.2. A faster fixed-parameter algorithm for trees -- 5. A polynomial-time algorithm for paths with a bounded number of colors -- 6. Hardness of approximation for trees -- 7. An exact algorithm for trees -- 8. Conclusion -- Bibliography -- Weak Markovian Bisimilarity: Abstracting from Prioritized/Weighted Internal Immediate Actions M. Bernardo and A. Aldini -- 1. Introduction -- 2. Extended Markovian Process Algebra -- 3. Weak Extended Markovian Bisimilarity -- 3.1. Extended Markovian Bisimilarity -- 3.2. Abstracting from Internal Immediate Actions -- 3.3. Congruence Result for Well-Prioritized Terms.

3.4. Axioms for Non-Recursive Well-Prioritized Terms -- 4. Conclusion -- References -- Analyzing Non-Interference with Respect to Classes D. Zanardini -- 1. Introduction -- 2. Preliminaries -- 3. Class-Oriented Abstract Non-Interference -- 4. ANI Analysis for Class Information -- 5. An Example -- 6. Conclusions and FutureWork -- References -- Computing Minimum Directed Feedback Vertex Set in O (1:9977n) I. Razgon -- 1. Introduction -- 2. Preliminaries -- 3. The Algorithm -- 4. Analysis -- Acknowledgements -- References -- Seeing the Trees and their Branches in the Network is Hard I. A. Kanj, L. Nakhleh, C. Than, and G. Xia -- 1. Introduction -- 2. Phylogenetic Networks, Trees, and the Infinite Site Model -- 3. Computational Complexity of the TC Problem -- 4. The ISPN Problem: Complexity and a Parameterized Algorithm -- 4.1. NP-completeness of ISPN -- 4.2. A Parameterized Algorithm for ISPN -- 5. The Cluster Containment Problem -- Bibliography -- Modeling Fuzzy Behaviours in Concurrent Systems L. D'Errico and M. Loreti -- 1. Introduction -- 2. Fuzzy Sets -- 3. Fuzzy Labelled Transition Systems -- 4. Fuzzy Hennessy-Milner Logic -- 4.1. FHML with recursion -- 5. Conclusions and FutureWorks -- Bibliography -- A Formal Framework for Compositional Compilation D. Ancona and E. Zucca -- 1. Introduction -- 2. An abstract framework -- 3. Linking by entailment -- 4. Compositional compilation and principal typings -- 5. Linking by environment entailment and subtyping -- 6. Conclusion -- Acknowledgements -- Bibliography -- Type Inference for Polymorphic Methods in Java-like Languages D. Ancona, G. Lagorio, and E. Zucca -- 1. Introduction -- 2. A type system with polymorphic method types -- 3. Inferring polymorphic method types -- 4. Related and further work -- Bibliography -- Sorting Streamed Multisets T. Gagie -- 1. Introduction -- 2. Algorithm -- 3. Lower Bound.

4. FutureWork -- Acknowledgments -- Bibliography -- An Analysis of a Simple Algorithm for Random Derangements D. Merlini, R. Sprugnoli, and M. C. Verri -- 1. Introduction -- 2. Derangements -- 3. The Triangle of First Fixed Points -- 4. Mean and Variance -- Acknowledgements -- Bibliography -- The Measure Hypothesis and Efficiency of Polynomial Time Approximation Schemes M. Hauptmann -- 1. Introduction -- 2. Preliminaries -- 3. Separating PTAS from EPTAS -- 4. Oracle Constructions -- 5. Conclusion -- Bibliography -- Dichotomy Results for Fixed Point Counting in Boolean Dynamical Systems S. Kosub and C. M. Homan -- 1. Introduction -- 2. The Dynamical Systems Framework -- 3. The Analysis Framework -- 3.1. Transition Classes -- 3.2. Network Classes -- 4. Islands of Tractability for Fixed Point Counting -- 4.1. The Case of Local Transition Functions Given By Lookup Tables -- 4.2. Succinctly Represented Local Transition Functions -- 5. Conclusion -- Bibliography -- Definable Sets in Weak Presburger Arithmetic C. Choffrut and A. Frigeri -- Introduction -- 1. Preliminaries -- 1.1. Variants of Presburger arithmetic -- 1.2. Logical definability -- 2. N-linear and Z-linear sets -- 2.1. Some notations -- 2.2. Linear sets -- 3. Properties of Z-linear sets -- 3.1. Closure properties -- 3.2. Quasisimple sets -- 4. Definable sets in weak Presburger arithmetic -- 4.1. An algebraic characterization of definable sets -- 4.2. A special case -- 4.3. The procedure -- Bibliography -- On Defining Proofs of Knowledge in the Bare Public-key Model G. Di Crescenzo and I. Visconti -- 1. Introduction -- 2. Defining Proofs of Knowledge in the BPK Model -- 3. Separating the Notions ofWitness Extraction -- 4. ConcurrentWitness Extraction -- Acknowledgments. -- Bibliography -- Author Index.