Foundations of Software Science and Computation Structures

1. Front Matter

   Pages I-XII

   PDF

2. Invited Paper

   1. Adequacy for Algebraic Effects

      • Gordon Plotkin, John Power

      Pages 1-24

3. Contributed Papers

   1. Secrecy Types for Asymmetric Communication

      • Martín Abadi, Bruno Blanchet

      Pages 25-41

   2. Axiomatizing Tropical Semirings

      • Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir

      Pages 42-56

   3. Type Isomorphisms and Proof Reuse in Dependent Type Theory

      • Gilles Barthe, Olivier Pons

      Pages 57-71

   4. On the Duality between Observability and Reachability

      • Michel Bidoit, Rolf Hennicker, Alexander Kurz

      Pages 72-87

   5. The Finite Graph Problem for Two-Way Alternating Automata

      • Mikolaj Bojańczyk

      Pages 88-103

   6. High-Level Petri Nets as Type Theories in the Join Calculus

      • Maria Grazia Buscemi, Vladimiro Sassone

      Pages 104-120

   7. Temporary Data in Shared Dataspace Coordination Languages

      • Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro

      Pages 121-136

   8. On Garbage and Program Logic

      • Cristiano Calcagno, Peter W. O’Hearn

      Pages 137-151

   9. The Complexity of Model Checking Mobile Ambients

      • Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot

      Pages 152-167

   10. The Rho Cube

       • Horatiu Cirstea, Claude Kirchner, Luigi Liquori

       Pages 168-183

   11. Type Inference with Recursive Type Equations

       • Mario Coppo

       Pages 184-198

   12. On the Modularity of Deciding Call-by-Need

       • Irène Durand, Aart Middeldorp

       Pages 199-213

   13. Synchronized Tree Languages Revisited and New Applications

       • Valérie Gouranton, Pierre Réty, Helmut Seidl

       Pages 214-229

   14. Computational Completeness of Programming Languages Based on Graph Transformation

       • Annegret Habel, Detlef Plump

       Pages 230-245

   15. Axioms for Recursion in Call-by-Value

       • Masahito Hasegawa, Yoshihiko Kakutani

       Pages 246-260

   16. Class Analysis of Object-Oriented Programs through Abstract Interpretation

       • Thomas Jensen, Fausto Spoto

       Pages 261-275

   17. On the Complexity of Parity Word Automata

       • Valerie King, Orna Kupferman, Moshe Y. Vardi

       Pages 276-286

   18. Foundations for a Graph-Based Approach to the Specification of Access Control Policies

       • Manuel Koch, Luigi Vincenzo Mancini, Francesco Parisi-Presicce

       Pages 287-302

ETAPS 2001 was the fourth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conferences. This year it comprised ve conferences (FOSSACS, FASE, ESOP, CC, TACAS), ten satellite workshops (CMCS, ETI Day, JOSES, LDTA, MMAABS, PFM, RelMiS, UNIGRA, WADT, WTUML), seven invited lectures, a debate, and ten tutorials. The events that comprise ETAPS address various aspects of the system de- lopment process, including speci cation, design, implementation, analysis, and improvement. The languages, methodologies, and tools which support these - tivities are all well within its scope. Di erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.

• Software engineering
• automata
• complexity
• complexity theory
• computational structures
• formal methods
• formal verification
• logic
• mathematical foundations
• model checking
• petri net
• programming
• programming language
• programming theory
• verification

• Dipartimento di Matematica e Informatica, Università di Udine, Udine, Italy

  Furio Honsell, Marino Miculan

Policies and ethics