Skip to content

Formal Semantics of Programming Languages An Introduction

Spend $50 to get a free DVD!

ISBN-10: 0262231697

ISBN-13: 9780262231695

Edition: 1993

Authors: Glynn Winskel

List price: $50.00
Blue ribbon 30 day, 100% satisfaction guarantee!
Out of stock
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!


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…    
Customers also bought

Book details

List price: $50.00
Copyright year: 1993
Publisher: MIT Press
Publication date: 2/5/1993
Binding: Hardcover
Pages: 384
Size: 7.50" wide x 9.50" long x 1.00" tall
Weight: 1.782
Language: English

Series foreword
Basic set theoryp. 1
Logical notationp. 1
Setsp. 2
Relations and functionsp. 6
Introduction to operational semanticsp. 11
IMP - a simple imperative languagep. 11
The evaluation of arithmetic expressionsp. 13
The evaluation of boolean expressionsp. 17
The execution of commandsp. 19
A simple proofp. 20
Alternative semanticsp. 24
Some principles of inductionp. 27
Mathematical inductionp. 27
Structural inductionp. 28
Well-founded inductionp. 31
Induction on derivationsp. 35
Definitions by inductionp. 39
Inductive definitionsp. 41
Rule inductionp. 41
Special rule inductionp. 44
Proof rules for operational semanticsp. 45
Operators and their least fixed pointsp. 52
The denotational semantics of IMPp. 55
Motivationp. 55
Denotational semanticsp. 56
Equivalence of the semanticsp. 61
Complete partial orders and continuous functionsp. 68
The Knaster-Tarski Theoremp. 74
The axiomatic semantics of IMPp. 77
The ideap. 77
The assertion language Assnp. 80
Semantics of assertionsp. 84
Proof rules for partial correctnessp. 89
Soundnessp. 91
Using the Hoare rules - an examplep. 93
Completeness of the Hoare rulesp. 99
Godel's Incompleteness Theoremp. 99
Weakest preconditions and expressivenessp. 100
Proof of Godel's Theoremp. 110
Verification conditionsp. 112
Predicate transformersp. 115
Introduction to domain theoryp. 119
Basic definitionsp. 119
Streams - an examplep. 121
Constructions on cpo'sp. 123
A metalanguagep. 135
Recursion equationsp. 141
The language RECp. 141
Operational semantics of call-by-valuep. 143
Denotational semantics of call-by-valuep. 144
Equivalence of semantics for call-by-valuep. 149
Operational semantics of call-by-namep. 153
Denotational semantics of call-by-namep. 154
Equivalence of semantics for call-by-namep. 157
Local declarationsp. 161
Techniques for recursionp. 163
Bekie's Theoremp. 163
Fixed-point inductionp. 166
Well-founded inductionp. 174
Well-founded recursionp. 176
Languages with higher typesp. 183
An eager languagep. 183
Eager operational semanticsp. 186
Eager denotational semanticsp. 188
Agreement of eager semanticsp. 190
A lazy languagep. 200
Lazy operational semanticsp. 201
Lazy denotational semanticsp. 203
Agreement of lazy semanticsp. 204
Fixed-point operatorsp. 209
Observations and full abstractionp. 215
Sumsp. 219
Information systemsp. 223
Recursive typesp. 223
Information systemsp. 225
Closed families and Scott predomainsp. 228
A cpo of information systemsp. 233
Constructionsp. 236
Recursive typesp. 251
An eager languagep. 251
Eager operational semanticsp. 255
Eager denotational semanticsp. 257
Adequacy of eager semanticsp. 262
The eager [lambda]-calculusp. 267
A lazy languagep. 278
Lazy operational semanticsp. 278
Lazy denotational semanticsp. 281
Adequacy of lazy semanticsp. 288
The lazy [lambda]-calculusp. 290
Nondeterminism and parallelismp. 297
Introductionp. 297
Guarded commandsp. 298
Communicating processesp. 303
Milner's CCSp. 308
Pure CCSp. 311
A specification languagep. 316
The modal [nu]-calculusp. 321
Local model checkingp. 327
A: Incompleteness and undecidabilityp. 337
Bibliographyp. 353
Indexp. 357
Table of Contents provided by Blackwell. All Rights Reserved.