This book solves several mathematical problems in the areas of Very Large Scale Integration (VLSI) and parallel computation. In particular, it describes optimal layouts for the shuffle-exchange graph, one of the best known networks for parallel computation. Attempts to design a shuffle-exchange computer have been hampered in part by the fact that, until now, no good layouts for the shuffle-exchange graph were known.

This book probes the stable marriage problem and its variants as a rich source of problems and ideas that illustrate both the design and analysis of efficient algorithms. It covers the most recent structural and algorithmic work on stable matching problems, simplifies and unifies many earlier proofs, strengthens several earlier results, and presents new results and more efficient algorithms.

Among the many approaches to formal reasoning about programs, Dynamic Logic enjoys the singular advantage of being strongly related to classical logic. Its variants constitute natural generalizations and extensions of classical formalisms. For example, Propositional Dynamic Logic (PDL) can be described as a blend of three complementary classical ingredients: propositional calculus, modal logic, and the algebra of regular events. In First-Order Dynamic Logic (DL), the propositional calculus is replaced by classical first-order predicate calculus.

This collection of original essays reflects the breadth of current research in computer science. Robin Milner, a major figure in the field, has made many fundamental contributions, particularly in theoretical computer science, the theory of programming languages, and functional programming languages.

Following a brief biography of Milner, the book contains five sections: Semantic Foundations, Programming Logic, Programming Languages, Concurrency, and Mobility. Together the pieces convey a seamless whole, ranging from highly abstract concepts to systems of great utility.

Written for advanced undergraduate and beginning graduate students, Foundations for Programming Languages uses a series of typed lambda calculi to study the axiomatic, operational, and denotational semantics of sequential programming languages. Later chapters are devoted to progressively more sophisticated type systems.

Algorithmic Number Theory provides a thorough introduction to the design and analysis of algorithms for problems from the theory of numbers. Although not an elementary textbook, it includes over 300 exercises with suggested solutions. Every theorem not proved in the text or left as an exercise has a reference in the notes section that appears at the end of each chapter. The bibliography contains over 1,750 citations to the literature.

Algebraic Semantics of Imperative Programs presents a self-contained and novel "executable" introduction to formal reasoning about imperative programs. The authors' primary goal is to improve programming ability by improving intuition about what programs mean and how they run.

The semantics of imperative programs is specified in a formal, implemented notation, the language OBJ; this makes the semantics highly rigorous yet simple, and provides support for the mechanical verification of program properties.

Control Flow Semantics presents a unified, formal treatment of the semantics of a wide spectrum of control flow notions as found in sequential, concurrent, logic, object-oriented, and functional programming languages.

Although the theory of object-oriented programming languages is far from complete, this book brings together the most important contributions to its development to date, focusing in particular on how advances in type systems and semantic models can contribute to new language designs.

The thirteen chapters written expressly for this book by logicians, theoretical computer scientists, philosophers, and semanticists address, from the perspective of mathematical logic, the problems of understanding and studying the flow of information through any information-processing system.

The Structure of Typed Programming Languages describes the fundamental syntactic and semantic features of modern programming languages, carefully spelling out their impacts on language design.

This mathematically oriented introduction to the theory of logic programming presents a systematic exposition of the resolution method for propositional, first-order, and Horn-clause logics, together with an analysis of the semantic aspects of the method. It is through the inference rule of resolution that both proofs and computations can be manipulated on computers, and this book contains elegant versions and proofs of the fundamental theorems and lemmas in the proof theory of logic programming.

At the 1900 International Congress of Mathematicians, held that year in Paris, the German mathematician David Hilbert put forth a list of 23 unsolved problems that he saw as being the greatest challenges for twentieth-century mathematics. Hilbert's 10th problem, to find a method (what we now call an algorithm) for deciding whether a Diophantine equation has an integral solution, was solved by Yuri Matiyasevich in 1970. Proving the undecidability of Hilbert's 10th problem is clearly one of the great mathematical results of the century.

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.

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.