Theoretical Aspects of Computer Software: 4th International Symposium, Tacs 2001, Sendai, Japan, October 2001, Proce Edings

by TACS 2001 (2001 : Sendai-shi, Miyagi-ken, Japan); Pierce, Benjamin C.

• ISBN13: 9783540427360
• ISBN10: 3540427368
• Format: Paperback
• Copyright: 2001-11-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the Fourth International Symposium on Theoretical Aspects of Computer Software, TACS 2001, held in Sendai, Japan, in October 2001. The book presents 21 selected and revised full papers. Also included are six invited papers plus one open lecture by internationally leading scientists. Among the topics addressed are automata theory, concurrency, control-flow analysis, lambda calculi, model checking and program logic.

Table of Contents

A Spatial Logic for Concurrency (Part I)	p. 1
Boxed Ambients	p. 38
A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation	p. 64
Formal Eavesdropping and Its Computational Interpretation	p. 82
Resource-Passing Concurrent Programming	p. 95
Solo Diagrams	p. 127
Observational Equivalence for Synchronized Graph Rewriting with Mobility	p. 145
Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness	p. 165
Termination Proofs and Complexity Certification	p. 183
A Renee Equation for Algorithmic Complexity	p. 201
Nominal Logic: A First Order Theory of Names and Binding	p. 219
A Logic Programming Language Based on Binding Algebras	p. 243
Proof-Search and Countermodel Generation in Propositional BI Logic	p. 263
Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders	p. 283
Modelisation of Timed Automata in Coq	p. 298
Model-Checking LTL with Regular Valuations for Pushdown Systems	p. 316
What Will Be Eventually True of Polynomial Hybrid Automata?	p. 340
Non-structural Subtype Entailment in Automata Theory	p. 360
Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems	p. 385
Weakest Congruence Results Concerning "Any-Lock"	p. 400
Design and Correctness of Program Transformations Based on Control-Flow Analysis	p. 420
Infinite Intersection and Union Types for the Lazy Lambda Calculus	p. 448
Strong Normalization of Second Order Symmetric Lambda-mu Calculus	p. 459
The Girard-Reynolds Isomorphism	p. 468
Lightweight Analysis of Object Interactions	p. 492
Typing Assembly Programs with Explicit Forwarding	p. 514
The UDP Calculus: Rigorous Semantics for Real Networking	p. 535
TACS Open Lecture
Unison: A File Synchronizer and Its Specification	p. 560
Author Index	p. 561
Table of Contents provided by Publisher. All Rights Reserved.