## Theoretical Aspects of Computer Software: 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001. ProceedingsNaoki Kobayashi, Benjamin C. Pierce 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). |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

A Spatial Logic for Concurrency | 1 |

Boxed Ambients | 38 |

A Typed Process Calculus for FineGrained Resource Access Control in Distributed Computation | 64 |

Formal Eavesdropping and Its Computational Interpretation | 82 |

ResourcePassing Concurrent Programming | 95 |

Solo Diagrams | 127 |

Observational Equivalence for Synchronized Graph Rewriting with Mobility | 145 |

FixedPoint Logic with the Approximation Modality and Its Kripke Completeness | 165 |

ModelChecking LTL with Regular Valuations for Pushdown Systems | 316 |

What Will Be Eventually True of Polynomial Hybrid Automata? | 340 |

Nonstructural Subtype Entailment in Automata Theory | 360 |

Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems | 385 |

Weakest Congruence Results Concerning AnyLock | 400 |

Design and Correctness of Program Transformations Based on ControlFlow Analysis | 420 |

Infinite Intersection and Union Types for the Lazy Lambda Calculus | 448 |

Strong Normalization of Second Order Symmetric Lambdamu Calculus | 459 |

Termination Proofs and Complexity Certification | 183 |

A Renee Equation for Algorithmic Complexity | 201 |

A First Order Theory of Names and Binding | 219 |

A Logic Programming Language Based on Binding Algebras | 243 |

ProofSearch and Countermodel Generation in Propositional BI Logic | 263 |

Generation of a Linear Time Query Processing Algorithm Based on WellQuasiOrders | 283 |

Modelisation of Timed Automata in Coq | 298 |

The GirardReynolds Isomorphism | 468 |

Lightweight Analysis of Object Interactions | 492 |

Typing Assembly Programs with Explicit Forwarding | 514 |

Rigorous Semantics for Real Networking | 535 |

A File Synchronizer and Its Specification | 560 |

561 | |

### Other editions - View all

### Common terms and phrases

abstract algebraic algorithm ambient apply arity atoms automata automaton axioms bisimulation calculus cap automata Computer Science concurrent configuration constraints construction constructors corresponding deﬁned Deﬁnition defunctionalization denote derivable domain encoding equivalence example expressions finite ﬁnite set ﬁrst first-order logic formula fresh function Functional Programming graph hybrid automaton induction hypothesis input labels lambda calculus Lecture Notes Lemma linear linear logic LNCS logic programming mobility mode model-checking multiset names nodes Nominal Logic Notes in Computer notion object variables operational semantics operator output parametric path predicate problem process calculi programming language proof properties Proposition provable pushdown systems reachable recursive reduction relation restricted result rewriting rules satisﬁes Scott domain semantics semi-decision procedures sequence socket Springer-Verlag structure subtyping symbol synchronization syntax Theorem theory transition type system valuation weakest congruence