Theoretical Basis of Programming Language Design

Author: Mitchell (USA)
Publisher:
Publish Date: 2006-11-01
Features: This book proposes a framework for analyzing the syntax, operational, and semantic properties of programming languages, which is based on a mathematical system called typed λ-calculus. The main features of λ-calculus are its notation for functions and other computable values, as well as an equational logic and a set of rules for expression evaluation. The simplest system in this book is an equational system called generalized algebra, which can be used to axiomatize and analyze many data types commonly used in programming. More advanced technical mechanisms, such as methods of logical relations, category theory, and the semantics of recursively defined types, are discussed in the middle chapters. The last three chapters of the book study polymorphic types, along with discussions on the formal specifications of abstract data types, program modules, type adaptation, and type inference. This book can serve as a textbook for advanced undergraduate or beginning graduate students in theoretical computer science, software systems, and mathematics, as well as a technical reference for higher research.