## Theories of Programming LanguagesThis textbook is a broad but rigorous survey of the theoretical basis for the design, definition, and implementation of programming languages, and of systems for specifying and proving program behavior. It encompasses imperative and functional programming, as well as the ways of integrating these aspects into more general languages. Basic concepts and their properties are described with mathematical rigor, but the mathematical development is balanced by numerous examples of applications, particularly of program specification and proof, concurrent programming, functional programming (including the use of continuations and lazy evaluation), and type systems (including subtyping, polymorphism, and modularization). Assuming only knowledge of elementary programming, this text is perfect for advanced undergraduate and beginning graduate courses in programming language theory, and will also 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

abstract application argument array assert assignment bool bound called Chapter comm command complex composition Computer concurrent conditional consider construction containing context continuation deﬁned deﬁnition denotes described discussed distinct domain DR SEM EQ element equivalence error evaluation example execution expression extend fact fail false ﬁnal ﬁnite ﬁrst formal function give given holds imperative inference rules inﬁnite initial integer intexp introduce judgement kind lambda calculus language least letrec limit list int logic maps meaning named newvar Notes numbers obtained occur operations output pair partial phrase polymorphic primitive procedure proof Proposition prove recursive reduction references relation result Section semantic equations sequence simple speciﬁcation step substitution subtyping Suppose syntax terminate transition true tuples variables write