## Theories of Programming LanguagesFirst published in 1998, this textbook is a broad but rigourous survey of the theoretical basis for the design, definition and implementation of programming languages and of systems for specifying and proving programme behaviour. Both imperative and functional programming are covered, as well as the ways of integrating these aspects into more general languages. Recognising a unity of technique beneath the diversity of research in programming languages, the author presents an integrated treatment of the basic principles of the subject. He identifies the relatively small number of concepts, such as compositional semantics, binding structure, domains, transition systems and inference rules, that serve as the foundation of the field. Assuming only knowledge of elementary programming and mathematics, this text is perfect for advanced undergraduate and beginning graduate courses in programming language theory and also will appeal to researchers and professionals in designing or implementing computer languages. |

### What people are saying - Write a review

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

### Contents

1 Predicate Logic | 1 |

2 The Simple Imperative Language | 24 |

3 Program Specifications and Their Proofs | 54 |

4 Arrays | 81 |

5 Failure InputOutput and Continuations | 97 |

6 Transition Semantics | 126 |

7 Nondeterminism and Guarded Commands | 136 |

8 SharedVariable Concurrency | 155 |

13 Iswimlike Languages | 273 |

14 A NormalOrder Language | 298 |

15 The Simple Type System | 315 |

16 Subtypes and Intersection Types | 349 |

17 Polymorphism | 379 |

18 Module Specification | 398 |

19 Algollike Languages | 415 |

Mathematical Background | 447 |

### Other editions - View all

### Common terms and phrases

Algol Algol 60 application argument array assert binary bool boolean boolexp called canonical form Chapter CN SEM EQ comm Computer Science concurrent conﬁguration construction constructor cont continuation semantics continuous function déf deﬁned deﬁnition denotational semantics described domain DR SEM EQ eager evaluation error example execution extend false ﬁelds ﬁnal result ﬁnite ﬁrst functional language give guarded commands inference rules input integer intersection types intexp intrinsic semantics intvar isomorphism lambda calculus lazy evaluation letrec list int listcase maps meaning metavariables natural numbers newvar nonterminal normal-order normal-order evaluation occur free operations output pair partial equivalence relations phrase polymorphic predicate logic predomain premisses programming languages proof Proposition satisﬁes semantic equations simple imperative language speciﬁcation Standard ML subtyping syntactic sugar terminate true tuples TY RULE TY SEM EQ tyerr type 9 type inference type inference rule type system typing judgement variable declarations zero