The formal semantics of programming languages : an introduction / Glynn Winskel.

Author
Winskel, G. (Glynn) [Browse]
Format
Book
Language
English
Published/​Created
  • Cambridge, Massachsuetts : MIT Press, [1993]
  • ©1993
Description
xviii, 361 pages : illustrations ; 24 cm

Availability

Copies in the Library

Location Call Number Status Location Service Notes
Engineering Library - Stacks QA76.7 .W555 1993 Browse related items Request

    Details

    Subject(s)
    Series
    Foundations of computing [More in this series]
    Summary note
    The Formal Semantics of Programming Languages provides the basic mathematical techniques necessary for those who are beginning a study of the semantics and logics of programming languages. These techniques will allow students to invent, formalize, and justify rules with which to reason about a variety of programming languages. Although the treatment is elementary, several of the topics covered are drawn from recent research, including the vital area of concurency. The book contains many exercises ranging from simple to miniprojects. Starting with basic set theory, structural operational semantics is introduced as a way to define the meaning of programming languages along with associated proof techniques. Denotational and axiomatic semantics are illustrated on a simple language of while-programs, and fall proofs are given of the equivalence of the operational and denotational semantics and soundness and relative completeness of the axiomatic semantics. A proof of Godel's incompleteness theorem, which emphasizes the impossibility of achieving a fully complete axiomatic semantics, is included. It is supported by an appendix providing an introduction to the theory of computability based on while-programs. Following a presentation of domain theory, the semantics and methods of proof for several functional languages are treated. The simplest language is that of recursion equations with both call-by-value and call-by-name evaluation. This work is extended to lan guages with higher and recursive types, including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship between denotational and operational semantics is stressed, and the proofs of the correspondence between the operation and denotational semantics are provided. The treatment of recursive types - one of the more advanced parts of the book - relies on the use of information systems to represent domains. The book concludes with a chapter on parallel programming languages, accompanied by a discussion of methods for specifying and verifying nondeterministic and parallel programs.
    Bibliographic references
    Includes bibliographical references (p. [353]-356) and index.
    Contents
    • Series foreword
    • Preface
    • 1 Basic set theory (starting p. 1)
    • 1.1 Logical notation (starting p. 1)
    • 1.2 Sets (starting p. 2)
    • 1.3 Relations and functions (starting p. 6)
    • 2 Introduction to operational semantics (starting p. 11)
    • 2.1 IMP
    • a simple imperative language (starting p. 11)
    • 2.2 The evaluation of arithmetic expressions (starting p. 13)
    • 2.3 The evaluation of boolean expressions (starting p. 17)
    • 2.4 The execution of commands (starting p. 19)
    • 2.5 A simple proof (starting p. 20)
    • 2.6 Alternative semantics (starting p. 24)
    • 3 Some principles of induction (starting p. 27)
    • 3.1 Mathematical induction (starting p. 27)
    • 3.2 Structural induction (starting p. 28)
    • 3.3 Well-founded induction (starting p. 31)
    • 3.4 Induction on derivations (starting p. 35)
    • 3.5 Definitions by induction (starting p. 39)
    • 4 Inductive definitions (starting p. 41)
    • 4.1 Rule induction (starting p. 41)
    • 4.2 Special rule induction (starting p. 44)
    • 4.3 Proof rules for operational semantics (starting p. 45)
    • 4.4 Operators and their least fixed points (starting p. 52)
    • 5 The denotational semantics of IMP (starting p. 55)
    • 5.1 Motivation (starting p. 55)
    • 5.2 Denotational semantics (starting p. 56)
    • 5.3 Equivalence of the semantics (starting p. 61)
    • 5.4 Complete partial orders and continuous functions (starting p. 68)
    • 5.5 The Knaster-Tarski Theorem (starting p. 74)
    • 6 The axiomatic semantics of IMP (starting p. 77)
    • 6.1 The idea (starting p. 77)
    • 6.2 The assertion language Assn (starting p. 80)
    • 6.3 Semantics of assertions (starting p. 84)
    • 6.4 Proof rules for partial correctness (starting p. 89)
    • 6.5 Soundness (starting p. 91)
    • 6.6 Using the Hoare rules
    • an example (starting p. 93)
    • 7 Completeness of the Hoare rules (starting p. 99)
    • 7.1 Godel's Incompleteness Theorem (starting p. 99)
    • 7.2 Weakest preconditions and expressiveness (starting p. 100)
    • 7.3 Proof of Godel's Theorem (starting p. 110)
    • 7.4 Verification conditions (starting p. 112)
    • 7.5 Predicate transformers (starting p. 115)
    • 8 Introduction to domain theory (starting p. 119)
    • 8.1 Basic definitions (starting p. 119)
    • 8.2 Streams
    • an example (starting p. 121)
    • 8.3 Constructions on cpo's (starting p. 123)
    • 8.4 A metalanguage (starting p. 135)
    • 9 Recursion equations (starting p. 141)
    • 9.1 The language REC (starting p. 141)
    • 9.2 Operational semantics of call-by-value (starting p. 143)
    • 9.3 Denotational semantics of call-by-value (starting p. 144)
    • 9.4 Equivalence of semantics for call-by-value (starting p. 149)
    • 9.5 Operational semantics of call-by-name (starting p. 153)
    • 9.6 Denotational semantics of call-by-name (starting p. 154)
    • 9.7 Equivalence of semantics for call-by-name (starting p. 157)
    • 9.8 Local declarations (starting p. 161)
    • 10 Techniques for recursion (starting p. 163)
    • 10.1 Bekie's Theorem (starting p. 163)
    • 10.2 Fixed-point induction (starting p. 166)
    • 10.3 Well-founded induction (starting p. 174)
    • 10.4 Well-founded recursion (starting p. 176)
    • 11 Languages with higher types (starting p. 183)
    • 11.1 An eager language (starting p. 183)
    • 11.2 Eager operational semantics (starting p. 186)
    • 11.3 Eager denotational semantics (starting p. 188)
    • 11.4 Agreement of eager semantics (starting p. 190)
    • 11.5 A lazy language (starting p. 200)
    • 11.6 Lazy operational semantics (starting p. 201)
    • 11.7 Lazy denotational semantics (starting p. 203)
    • 11.8 Agreement of lazy semantics (starting p. 204)
    • 11.9 Fixed-point operators (starting p. 209)
    • 11.10 Observations and full abstraction (starting p. 215)
    • 11.11 Sums (starting p. 219)
    • 12 Information systems (starting p. 223)
    • 12.1 Recursive types (starting p. 223)
    • 12.2 Information systems (starting p. 225)
    • 12.3 Closed families and Scott predomains (starting p. 228)
    • 12.4 A cpo of information systems (starting p. 233)
    • 12.5 Constructions (starting p. 236)
    • 13 Recursive types (starting p. 251)
    • 13.1 An eager language (starting p. 251)
    • 13.2 Eager operational semantics (starting p. 255)
    • 13.3 Eager denotational semantics (starting p. 257)
    • 13.4 Adequacy of eager semantics (starting p. 262)
    • 13.5 The eager [lambda]-calculus (starting p. 267)
    • 13.6 A lazy language (starting p. 278)
    • 13.7 Lazy operational semantics (starting p. 278)
    • 13.8 Lazy denotational semantics (starting p. 281)
    • 13.9 Adequacy of lazy semantics (starting p. 288)
    • 13.10 The lazy [lambda]-calculus (starting p. 290)
    • 14 Nondeterminism and parallelism (starting p. 297)
    • 14.1 Introduction (starting p. 297)
    • 14.2 Guarded commands (starting p. 298)
    • 14.3 Communicating processes (starting p. 303)
    • 14.4 Milner's CCS (starting p. 308)
    • 14.5 Pure CCS (starting p. 311)
    • 14.6 A specification language (starting p. 316)
    • 14.7 The modal [nu]-calculus (starting p. 321)
    • 14.8 Local model checking (starting p. 327)
    • A: Incompleteness and undecidability (starting p. 337)
    • Bibliography (starting p. 353)
    • Index (starting p. 357)
    ISBN
    • 0262231697
    • 9780262231695
    • 0262731037
    • 9780262731034
    LCCN
    92036718
    OCLC
    26764522
    International Article Number
    • 9780262731034
    Statement on language in description
    Princeton University Library aims to describe library materials in a manner that is respectful to the individuals and communities who create, use, and are represented in the collections we manage. Read more...
    Other views
    Staff view