[Prev][Next][Index][Thread]
Book by Carl Gunter
Date: Mon, 28 Sep 92 16:40 EDT
My graduate-level textbook on the semantics of programming languages
is now available. I append below the title and publisher, a copy of
the table of contents, an abstract from the preface of the book, and,
at the end of the message, information on how to order it.
[I taught from a draft of this book last term. It is a masterful,
beautifully polished graduate text in semantics, which I recommend with
enthusiasm.
Yours truly,
Prof. Albert R. Meyer
MIT Lab. for Computer Science
Moderator, types@theory.lcs.mit.edu]
------------------------------------------------------------------------
Semantics of Programming Languages : Structures and Techniques
Carl A. Gunter, MIT Press Foundations of Computing Series, xx+419 pages.
@book{GUNTER92BOOK,
author = "C. A. Gunter",
title = "Semantics of Programming Languages: Structures and Techniques",
publisher = "MIT Press",
series = "Foundations of Computing",
year = "1992"}
------------------------------------------------------------------------
SEMANTICS OF PROGRAMMING LANGUAGES
Structures and Techniques
List of Tables
List of Figures
Series Foreword
Preface
1. Introduction 1
1.1 Semantics
1.2 Semantics of Programming Languages
1.3 Notes
2. The Simply-Typed Lambda-Calculus 31
2.1 Syntax of Lambda-Terms
2.2 Rules
2.3 Models
2.4 Notes
3. Categorical Models of Simple Types 63
3.1 Products and Cartesian Closure
3.2 Lambda-Calculus with Constants
and Products
3.3 The Use of Category Theory
3.4 Notes
4. Recursive Definitions of Functions 97
4.1 A Programming Language for
Computable Functions
4.2 Fixed Points in Complete Partial Orders
4.3 Fixed-Point Semantics of PCF
4.4 Bounded Recursion
4.5 Notes
5. Two Theories of Finite Approximation 145
5.1 Bc-domains
5.2 Stable functions and dI-domains
5.3 Equivalences between categories.
5.4 Notes
6. Relating Interpretations 177
6.1 Full Abstraction
6.2 Extensions of Adequacy Results
6.3 Products and Sums
6.4 Notes
7. Types and Evaluation 217
7.1 Expressiveness
7.2 Security
7.3 Reference types
7.4 Recursive Types
7.5 ML Polymorphism and Type Inference
7.6 Notes
8. Universal Domains 255
8.1 Untyped lambda-Calculus
8.2 Domain Equations
8.3 Notes
9. Subtype Polymorphism 285
9.1 Subtypes as Subsets
9.2 Subsumption as Implicit Coercion
9.3 Notes
10. Domain Theory 315
10.1 Fixed Points of Functors
10.2 Bifinite domains
10.3 Adjunctions and Powerdomains
10.5 Notes
11. Parametric Polymorphism 357
11.1 Calculi for Expressing Parametric
Polymorphism
11.2 Indexed Families of Domains
11.3 Notes
List of Notations 391
Bibliography 395
Subject Index 407
------------------------------------------------------------------------
ABSTRACT FROM PREFACE
This book expounds the basic motivations and philosophy underlying the
applications of semantic techniques in programming language theory.
There is an emphasis on the structures used in semantics and the
techniques that have been developed for relating various approaches to
the semantics of programming languages, particularly for languages
with higher-order functions. Type systems are the central
organizational theme of the dicussion.
The book is designed as a text for upper-level and graduate-level
students from all areas of computer science; it should also be useful
to anyone needing an easily accessed description of fundamental
results and calculi from the semantics of programming languages. Some
of the primary topics covered here include models of types,
operational semantics, category theory, domain theory, fixed-point
(denotational) semantics, full abstraction and other semantic
correspondence criteria, relationships between types and evaluation,
type checking and inference, subtypes, and parametric polymorphism.
As a set of general prerequisites for the book I assume familiarity
with the basic concepts of programming languages such as variable
binding and scope, evaluation, and parsing. Some familiarity with
interpreters and compilers is also expected. Ideally, a multi-lingual
student should know something about Lisp (or Scheme), Prolog, and an
imperative language such as Pascal or C. Knowledge of a language
based on the typed lambda-calculus such as ML or Haskell would be
helpful (especially for Chapter 7) but it is not assumed. The text by
Paulson ("ML for the Working Computer Scientist", Cambridge University
Press, 1991) is a representative discussion of ML programming. For
computer science students, this book can serve as an introduction to
the mathematical techniques used in the study of programming
languages. Some mathematical sophistication is essential, but I have
limited the prerequisites to what a student should have encountered
already in an undergraduate course on logic or abstract algebra. In
summary, general familiarity with a representative from each of the
following groups of texts forms an ideal background:
1. Compilers and interpreters
* Aho, Sethi, and Ullman, "Compilers: Principles, Techniques, and
Tools", Addison Wesley, 1985;
* Fischer and LeBlanc, Crafting a Compiler with C, Benjamin/Cummings,
1991.
2. Comparative programming languages
* Sethi, "Programming Languages: Concepts and Constructs", Addison
Wesley, 1989;
* Kamin, "Programming Languages: An Interpreter Based Approach",
Addison Wesley, 1990;
* Friedman, Wand, and Haynes, Essentials of Programming Languages,
MIT Press, 1992.
3. Logic
* Boolos and Jeffrey, "Computability and Logic", Cambridge University
Press, second edition, 1980;
* Lewis and Papadimitriou, "Elements of the Theory of Computation",
Prentice-Hall, 1981.
In general, the contents of the book is self-contained with enough
information that a diligent reader can derive full proofs of all the
results with enough time, pencils, and paper. A wide selection of
exercises have been provided at the ends of the sections in which the
definitions and methods they draw upon are stated. At the end of each
chapter there is a section of notes in which references to work
related to the topic of the chapter are given.
------------------------------------------------------------------------
Available at local bookshops or contact the following to order:
In North America $37.50 Cloth ISBN 0-262-07143-6
Toll Free Number 1-800-356-0343
The MIT Press
55 Hayward Street
Cambridge, MA 02142-1399
U.S.A.
Sawabini@MIT.EDU We are unable to accept orders via e-mail.
For information on purchase and price outside North America contact:
Maureen Curtin
International Department
The MIT Press
55 Hayward Street
Cambridge, MA 02142-1399
U.S.A.
Curtin@MIT.EDU We are unable to accept orders via e-mail.
Examination copies are available at the discretion of The MIT Press to
qualified instructors of appropriate courses. If you would like to
consider this text for course adoption which would result in 12 or more
student purchases, please write to the address above with the following
course information: course title, enrollment, level, course commencement
date, and previous text(s).