| Preface | p. ix |
| About the illustrations | p. xiii |
| List of illustrations | p. xiv |
| List of tables | p. xv |
| Background | p. 1 |
| A question of semantics | p. 3 |
| Semantics is the study of meaning | p. 3 |
| Examples from the history of programming language | p. 4 |
| Different approaches to program semantics | p. 6 |
| Applications of program semantics | p. 10 |
| Mathematical preliminaries | p. 16 |
| Mathematical induction | p. 16 |
| Logical notation | p. 17 |
| Sets | p. 19 |
| Operations on sets | p. 20 |
| Relations | p. 21 |
| Functions | p. 22 |
| First Examples | p. 25 |
| The basic principles | p. 27 |
| Abstract syntax | p. 27 |
| Transition systems | p. 30 |
| Big-step vs. small-step semantics | p. 31 |
| Operational semantics of arithmetic expressions | p. 31 |
| Proving properties | p. 38 |
| A semantics of Boolean expressions | p. 39 |
| The elements of an operational semantics | p. 40 |
| Basic imperative statements | p. 43 |
| Program states | p. 43 |
| A big-step semantics of statements | p. 45 |
| A small-step semantics of statements in Bims | p. 53 |
| Equivalence of the two semantics | p. 55 |
| Two important proof techniques | p. 60 |
| Language Constructs | p. 63 |
| Control structures | p. 65 |
| Some general assumptions | p. 65 |
| Loop constructs | p. 66 |
| Semantic equivalence | p. 70 |
| Abnormal termination | p. 72 |
| Nondeterminism | p. 73 |
| Concurrency | p. 76 |
| Blocks and procedures (1) | p. 79 |
| Abstract syntax of Bip | p. 79 |
| The environment-store model | p. 80 |
| Arithmetic and Boolean expressions | p. 83 |
| Declarations | p. 84 |
| Statements | p. 85 |
| Scope rules | p. 86 |
| Parameters | p. 94 |
| The language Bump | p. 94 |
| Call-by-reference | p. 96 |
| On recursive and non-recursive procedure calls | p. 97 |
| Call-by-value | p. 99 |
| Call-by-name | p. 100 |
| A comparison of parameter mechanisms | p. 110 |
| Concurrent communicating processes | p. 113 |
| Channel-based communication - Cab | p. 113 |
| Global and local behaviour | p. 114 |
| Synchronous communication in Cab | p. 115 |
| Other communication models | p. 119 |
| Bisimulation equivalence | p. 122 |
| Channels as data - the -calculus | p. 123 |
| Structured declarations | p. 134 |
| Records | p. 134 |
| The language Bur | p. 135 |
| The class-based language Coat | p. 142 |
| Blocks and procedures (2) | p. 154 |
| Run-time stacks | p. 154 |
| Declarations | p. 155 |
| Statements | p. 155 |
| Concurrent object-oriented languages | p. 161 |
| The language Cola | p. 161 |
| A small-step semantics of concurrent behaviour | p. 163 |
| Transition systems | p. 163 |
| Functional programming languages | p. 171 |
| What is a functional programming language? | p. 171 |
| Historical background | p. 173 |
| The -calculus | p. 174 |
| Flan - a simple functional language | p. 177 |
| Further reading | p. 181 |
| Related Topics | p. 183 |
| Typed programming languages | p. 185 |
| Type systems | p. 185 |
| Typed Bump | p. 187 |
| Typed Flan | p. 198 |
| Type polymorphism and type inference | p. 209 |
| An introduction to denotational semantics | p. 211 |
| Background | p. 211 |
| -Notation | p. 212 |
| Basic ideas | p. 214 |
| Denotational semantics of statements | p. 216 |
| Further reading | p. 220 |
| Recursive definitions | p. 222 |
| A first example | p. 222 |
| A recursive definition specifies a fixed-point | p. 224 |
| The fixed-point theorem | p. 225 |
| How to apply the fixed-point theorem | p. 231 |
| Examples of cpos | p. 232 |
| Examples of continuous functions | p. 236 |
| Examples of computations of fixed-points | p. 240 |
| An equivalence result | p. 241 |
| Other applications | p. 246 |
| Further reading | p. 248 |
| A big-step semantics of Bip | p. 249 |
| Implementing semantic definitions in SML | p. 257 |
| References | p. 264 |
| Index | p. 269 |
| Table of Contents provided by Ingram. All Rights Reserved. |