Theoretical Aspects of Computer Software

1. Front Matter

   Pages I-XV

   PDF

2. Invited Talk 1

   1. A Spatial Logic for Concurrency (Part I)

      • Luís Caires, Luca Cardelli

      Pages 1-37

3. Session 1

   1. Boxed Ambients

      • Michele Bugliesi, Giuseppe Castagna, Silvia Crafa

      Pages 38-63

   2. A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation

      • Daisuke Hoshina, Eijiro Sumii, Akinori Yonezawa

      Pages 64-81

   3. Formal Eavesdropping and Its Computational Interpretation

      • Martín Abadi, Jan Jürjens

      Pages 82-94

4. Invited Talk 2

   1. Resource-Passing Concurrent Programming

      • Kazunori Ueda

      Pages 95-126

5. Session 2

   1. Solo Diagrams

      • Cosimo Laneve, Joachim Parrow, Björn Victor

      Pages 127-144

   2. Observational Equivalence for Synchronized Graph Rewriting with Mobility

      • Barbara König, Ugo Montanari

      Pages 145-164

6. Session 3

   1. Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness

      • Hiroshi Nakano

      Pages 165-182

   2. Termination Proofs and Complexity Certification

      • Daniel Leivant

      Pages 183-200

   3. A Renee Equation for Algorithmic Complexity

      • Keye Martin

      Pages 201-218

7. Invited Talk 3

   1. Nominal Logic: A First Order Theory of Names and Binding

      • Andrew M. Pitts

      Pages 219-242

8. Session 4

   1. A Logic Programming Language Based on Binding Algebras

      • Makoto Hamana

      Pages 243-262

   2. Proof-Search and Countermodel Generation in Propositional BI Logic

      • Didier Galmiche, Daniel Méry

      Pages 263-282

   3. Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders

      • Mizuhito Ogawa

      Pages 283-297

9. Invited Talk 4

   1. Modelisation of Timed Automata in Coq

      • Christine Paulin-Mohring

      Pages 298-315

10. Session 5

    1. Model-Checking LTL with Regular Valuations for Pushdown Systems

       • Javier Esparza, Antonín Kučera, Stefan Schwoon

       Pages 316-339

    2. What Will Be Eventually True of Polynomial Hybrid Automata?

       • Martin Fränzle

       Pages 340-359

    3. Non-structural Subtype Entailment in Automata Theory

       • Joachim Niehren, Tim Priesnitz

       Pages 360-384

11. Session 6

    1. Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems

       • Ph. Schnoebelen

       Pages 385-399

This volume constitutes the proceedings of the Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 2001) held at Tohoku U- versity, Sendai, Japan in October 2001. The TACS symposium focuses on the theoretical foundations of progr- ming and their applications. As this volume shows, TACS is an international symposium, with participants from many di?erent institutions and countries. TACS 2001 was the fourth symposium in the TACS series, following TACS’91, TACS’94, and TACS’97, whose proceedings were published as Volumes 526, 789, and 1281, respectively, of Springer-Verlag’s Lecture Notes in Computer Science series. The TACS 2001 technical program consisted of invited talks and contributed talks. In conjunction with this program there was a special open lecture by Benjamin Pierce; this lecture was open to non-registrants. TACS 2001 bene?ted from the e?orts of many people; in particular, members of the Program Committee and the Organizing Committee. Our special thanks go to the Program Committee Co-chairs: Naoki Kobayashi (Tokyo Institute of Technology) Benjamin Pierce (University of Pennsylvania).

• Action Calculi
• Automat
• Concurrency
• Control-Flow Analysis
• Model Checking
• Program Logic
• Program Semantics
• automata
• lambda calculus
• logic

• Department of Computer Science, Tokyo Institute of Technology Graduate School of Information Science and Engineering, Tokyo, Japan

  Naoki Kobayashi

• Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA

  Benjamin C. Pierce

Policies and ethics