Theoretical aspects of computer software. 4th international symposium, TACS 2001, Sendai, Japan, October 29--31, 2001. Proceedings. (Q1880418)

The articles of this volume will be reviewed individually. The preceding symposium has been reviewed (see Zbl 0871.00032) Indexed articles: \textit{Caires, Luís; Cardelli, Luca}, A spatial logic for concurrency. I., 1-37 [Zbl 1087.03507] \textit{Bugliesi, Michele; Castagna, Giuseppe; Crafa, Silvia}, Boxed ambients, 38-63 [Zbl 1087.68541] \textit{Hoshina, Daisuke; Sumii, Eijiro; Yonezawa, Akinori}, A typed process calculus for fine-grained resource access control in distributed computation, 64-81 [Zbl 1087.68605] \textit{Abadi, Martín; Jürjens, Jan}, Formal eavesdropping and its computational interpretation, 82-94 [Zbl 1087.68563] \textit{Ueda, Kazunori}, Resource-passing concurrent programming, 95-126 [Zbl 1087.68547] \textit{Laneve, Cosimo; Parrow, Joachim; Victor, Björn}, Solo diagrams, 127-144 [Zbl 1087.68607] \textit{König, Barbara; Montanari, Ugo}, Observational equivalence for synchronized graph rewriting with mobility, 145-164 [Zbl 1087.68606] \textit{Nakano, Hiroshi}, Fixed-point logic with the approximation modality and its Kripke completeness, 165-182 [Zbl 1087.68546] \textit{Leivant, Daniel}, Termination proofs and complexity certification, 183-200 [Zbl 1087.68545] \textit{Martin, Keye}, A renee equation for algorithmic complexity, 201-218 [Zbl 1087.68558] \textit{Pitts, Andrew M.}, Nominal logic: A first order theory of names and binding, 219-242 [Zbl 1087.03510] \textit{Hamana, Makoto}, A logic programming language based on binding algebras, 243-262 [Zbl 1087.68529] \textit{Galmiche, Didier; Méry, Daniel}, Proof-search and countermodel generation in propositional BI logic, 263-282 [Zbl 1087.03509] \textit{Ogawa, Mizuhito}, Generation of a linear time query processing algorithm based on well-quasi-orders, 283-297 [Zbl 1087.68561] \textit{Paulin-Mohring, Christine}, Modelisation of timed automata in Coq, 298-315 [Zbl 1087.68575] \textit{Esparza, Javier; Kučera, Antonín; Schwoon, Stefan}, Model-checking LTL with regular valuations for pushdown systems, 316-339 [Zbl 1087.68542] \textit{Fränzle, Martin}, What will be eventually true of polynomial hybrid automata?, 340-359 [Zbl 1087.68571] \textit{Niehren, Joachim; Priesnitz, Tim}, Non-structural subtype entailment in automata theory, 360-384 [Zbl 1087.68524] \textit{Schnoebelen, Ph.}, Bisimulation and other undecidable equivalences for lossy channel systems, 385-399 [Zbl 1087.68609] \textit{Puhakka, Antti}, Weakest congruence results concerning ``any-lock'', 400-419 [Zbl 1087.68608] \textit{Banerjee, Anindya; Heintze, Nevin; Riecke, Jon G.}, Design and correctness of program transformations based on control-flow analysis, 420-447 [Zbl 1087.68540] \textit{Bonsangue, Marcello M.; Kok, Joost N.}, Infinite intersection and union types for the lazy lambda calculus, 448-458 [Zbl 1087.68536] \textit{Yamagata, Yoriyuki}, Strong normalization of second order symmetric lambda-mu calculus, 459-467 [Zbl 1087.68538] \textit{Wadler, Philip}, The Girard-Reynolds isomorphism, 468-491 [Zbl 1087.68537] \textit{Jackson, Daniel; Fekete, Alan}, Lightweight analysis of object interactions, 492-513 [Zbl 1087.68539] \textit{Beringer, Lennart}, Typing assembly programs with explicit forwarding, 514-534 [Zbl 1087.68548] \textit{Serjantov, Andrei; Sewell, Peter; Wansbrough, Keith}, The UDP calculus: Rigorous semantics for real networking, 535-559 [Zbl 1087.68555] \textit{Pierce, Benjamin C.; Vouillon, Jérôme}, Unison: A file synchronizer and its specification, 560 [Zbl 1087.68554]