From: carl@research.att.com (Carl Gunter)
Newsgroups: fj.mail-lists.types
Subject: Book by Carl Gunter
Date: 29 Sep 92 14:59:18 GMT
Distribution: fj

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).