| Theoretical Computer Science and Software Science: The Past, the Present and the Future | p. 3 |
| Future Trends of TAPSOFT | p. 6 |
| New Challenges for Theoretical Computer Science | p. 11 |
| What Does the Future Hold for Theoretical Computer Science? | p. 15 |
| Automata Theory on Trees and Partial Orders | p. 20 |
| A Theory of Testing for Timed Automata | p. 39 |
| Conservative Extensions, Interpretations Between Theories and All That | p. 40 |
| Specification and Proof in Membership Equational Logic | p. 67 |
| Formalism and Method | p. 93 |
| CoFI: The Common Framework Initiative for Algebraic Specification and Development | p. 115 |
| Logicality of Conditional Rewrite Systems | p. 141 |
| Simulating Forward-Branching Systems with Constructor Systems | p. 153 |
| Reliable Generalized and Context Dependent Commutation Relations | p. 165 |
| Word-into-Trees Transducers with Bounded Difference | p. 177 |
| Generalized Quantitative Temporal Reasoning: An Automata-Theoretic Approach | p. 189 |
| The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and Their Model-Checking in High-Level Languages | p. 201 |
| Model Checking Through Symbolic Reachability Graph | p. 213 |
| Optimal Implementation of Wait-Free Binary Relations | p. 225 |
| Relative Undecidability in the Termination Hierarchy of Single Rewrite Rules | p. 237 |
| Termination Proofs Using gpo Ordering Constraints | p. 249 |
| Automatically Proving Termination Where Simplification Orderings Fail | p. 261 |
| Generating Efficient, Terminating Logic Programs | p. 273 |
| Modal Characterization of Weak Bisimulation for Higher-Order Processes | p. 285 |
| Formats of Ordered SOS Rules with Silent Actions | p. 297 |
| A Uniform Syntactical Method for Proving Coinduction Principles in Lambda-calculi | p. 309 |
| A Labelled Transition Systems for pi-epsilon-Calculus | p. 321 |
| Set Operations for Recurrent Term Schematizations | p. 333 |
| Inclusion Constraints over Non-empty Sets of Trees | p. 345 |
| Grid Structures and Undecidable Constraint Theories | p. 357 |
| Predicative Functional Recurrence and Poly-space | p. 369 |
| On the Complexity of Function Pointer May-Alias Analysis | p. 381 |
| Maximum Packing for Biconnected Outerplanar Graphs | p. 393 |
| Synchronization of a Line of Identical Processors at a Given Time | p. 405 |
| An Algorithm for the Solution of Tree Equations | p. 417 |
| E-unification by Means of Tree Tuple Synchronized Grammars | p. 429 |
| Linear Interpolation for the Higher-Order Matching Problem | p. 441 |
| A Semantic Framework for Functional Logic Programming with Algebraic Polymorphic Types | p. 453 |
| Subtyping Constraints for Incomplete Objects | p. 465 |
| Partializing Stone Spaces Using SFP Domains | p. 478 |
| Let-Polymorphism and Eager Type Schemes | p. 490 |
| Semantics of Architectural Connectors | p. 505 |
| Protective Interface Specifications | p. 520 |
| Specifying Complex and Structured Systems with Evolving Algebras | p. 535 |
| A Comparison of Modular Verification Techniques | p. 550 |
| A Compositional Proof of a Real-Time Mutual Exclusion Protocol | p. 565 |
| Traces of I/O-Automata in Isabelle/HOLCF | p. 580 |
| Reactive Types | p. 595 |
| A Type-Based Approach to Program Security | p. 607 |
| An Applicative Module Calculus | p. 622 |
| Compositional Specification of Embedded Systems with Statecharts | p. 637 |
| Verification of Message Sequence Charts via Template Matching | p. 652 |
| Probabilistic Lossy Channel Systems | p. 667 |
| A Logic of Object-Oriented Programs | p. 682 |
| Auxiliary Variables and Recursive Procedures | p. 697 |
| Locality Based Linda: Programming with Explicit Localities | p. 712 |
| A Syntactic Theory of Dynamic Binding | p. 727 |
| A Unified Framework for Binding-Time Analysis | p. 742 |
| A Typed Intermediate Language for Flow-Directed Compilation | p. 757 |
| Action Refinement as an Implementation Relation | p. 772 |
| Behaviour-Refinement of Coalgebraic Specifications with Conductive Correctness Proofs | p. 787 |
| COMPASS: A Comprehensible Assertion Method | p. 803 |
| Using LOTOS Patterns to Characterize Architectural Styles | p. 818 |
| Automating Formal Specification-Based Testing | p. 833 |
| Typelab: An Environment for Modular Program Development | p. 851 |
| TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving | p. 855 |
| Proving System Correctness with KIV | p. 859 |
| A New Proof-Manager and Graphic Interface for the Larch Prover | p. 863 |
| A Web-Based Animator for Object Specifications in a Persistent Environment | p. 867 |
| Publishing Formal Specifications in Z Notation on World Wide Web | p. 871 |
| DOSFOP - A Documentation Tool for the Algebraic Programming Language Opal | p. 875 |
| AG: A Set of Maple Packages for Symbolic Computing of Automata and Semigroups | p. 879 |
| Author Index | p. 883 |
| Table of Contents provided by Blackwell. All Rights Reserved. |
