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).
Author(s): Luís Caires, Luca Cardelli (auth.), Naoki Kobayashi, Benjamin C. Pierce (eds.)
Series: Lecture Notes in Computer Science 2215
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2001
Language: English
Pages: 565
Tags: Logics and Meanings of Programs; Software Engineering/Programming and Operating Systems; Mathematical Logic and Formal Languages
A Spatial Logic for Concurrency (Part I)....Pages 1-37
Boxed Ambients....Pages 38-63
A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation....Pages 64-81
Formal Eavesdropping and Its Computational Interpretation....Pages 82-94
Resource-Passing Concurrent Programming....Pages 95-126
Solo Diagrams....Pages 127-144
Observational Equivalence for Synchronized Graph Rewriting with Mobility....Pages 145-164
Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness....Pages 165-182
Termination Proofs and Complexity Certification....Pages 183-200
A Renee Equation for Algorithmic Complexity....Pages 201-218
Nominal Logic: A First Order Theory of Names and Binding....Pages 219-242
A Logic Programming Language Based on Binding Algebras....Pages 243-262
Proof-Search and Countermodel Generation in Propositional BI Logic....Pages 263-282
Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders....Pages 283-297
Modelisation of Timed Automata in Coq....Pages 298-315
Model-Checking LTL with Regular Valuations for Pushdown Systems....Pages 316-339
What Will Be Eventually True of Polynomial Hybrid Automata?....Pages 340-359
Non-structural Subtype Entailment in Automata Theory....Pages 360-384
Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems....Pages 385-399
Weakest Congruence Results Concerning “Any-Lock”....Pages 400-419
Design and Correctness of Program Transformations Based on Control-Flow Analysis....Pages 420-447
Infinite Intersection and Union Types for the Lazy Lambda Calculus....Pages 448-458
Strong Normalization of Second Order Symmetric Lambda-mu Calculus....Pages 459-467
The Girard-Reynolds Isomorphism....Pages 468-491
Lightweight Analysis of Object Interactions....Pages 492-513
Typing Assembly Programs with Explicit Forwarding....Pages 514-534
The UDP Calculus: Rigorous Semantics for Real Networking....Pages 535-559
Unison: A File Synchronizer and Its Specification....Pages 560-560
