# Semantics of Programming Languages

## Overview

*Semantics of Programming Languages *exposes the basic motivations and philosophy underlying the applications of semantic techniques in computer science. It introduces the mathematical theory of programming languages with an emphasis on higher-order functions and type systems. Designed as a text for upper-level and graduate-level students, the mathematically sophisticated approach will also prove useful to professionals who want an easily referenced description of fundamental results and calculi.

Basic connections between computational behavior, denotational semantics, and the equational logic of functional programs are thoroughly and rigorously developed. Topics covered include models of types, operational semantics, category theory, domain theory, fixed point (denotational). semantics, full abstraction and other semantic correspondence criteria, types and evaluation, type checking and inference, parametric polymorphism, and subtyping. All topics are treated clearly and in depth, with complete proofs for the major results and numerous exercises.

## About the Author

Carl A. Gunter is Professor in the Department of Computer and Information Science at the University of Pennsylvania.

## Endorsements

"Gunter's book treats the essence of programming language theory—the span between the "meaning" of a computer program, and the concrete and intricate ways in which programs are executed by a machine. He brings together the established theoretical advances in this range. It is rewarding for someone who has played a small part in these developments to see them laid out so expertly, and with such pedagogic concern; readers new to the field—and many who already know a lot about it—will also be rewarded by following its carefully designed path."

—**Robin Milner**, University of Edinburgh

“Carl Gunter’s *Semantics of Programming Languages* is a much-needed resource for students, researchers, and designers of programming languages. It is both broader and deeper than previous books on the semantics of programming languages, and it collects important research developments in a carefully organized, accessible form. Its balanced treatment of operational and denotational approaches, and its coverage of recent work in type theory are particularly welcome.”

—**David MacQueen**, Head, Software Principles Department, AT&T Bell Laboratories, Murray Hill, New Jersey

“*Semantics of Programming Languages* by Carl Gunter, is an outstanding exposition of the mathematical definition of functional programming languages, and of the underlying theory of domains. It combines the clarity needed for an advanced textbook with a thoroughness that should make it a standard reference work.”

—**John C. Reynolds**, Professor of Computer Science, Carnegie Mellon University

“*Semantics of Programming Languages* is a worthy successor to Stoy and Schmidt. It is an ideal way for researchers in programming languages and advanced graduate students to learn both modern semantics and category theory. I have used a very early draft of a few chapters with some success in an advanced graduate class at Iowa State University. I am glad that Professor Gunter has added more introductory material, and also more detail on type theory. The book has a balanced treatment of operational and fixed point semantics, which reflects the growing importance of operational semantics. The book has excellent pointers into the literature.”

—**Gary Leavens**, Department of Computer Science, Iowa State University

“Carl Gunter’s *Semantics of Programming Languages* is a readable and carefully worked out introduction to essential concepts underlying a mathematical study of programming languages. Topics include models of the lambda calculus, operational semantics, domains, full abstractions, and polymorphism. The tone, selection of material, and exercises are just right—the reader experiences an appealing and rigorous, but not overwhelming, development of fundamental concepts.”

—**Neil D. Jones**, Professor of DIKU (Computer Science Department), the University of Copenhagen