Albert Meyer

  • Research Directions in Computer Science, Second Edition

    An MIT Perspective

    John V. Guttag, Albert Meyer, Ronald L. Rivest, and Peter Szolovits

    Research Directions in Computer Science celebrates the twenty-fifth anniversary of the founding of MIT's Project MAC. It covers the full range of ongoing computer science research at the MIT Laboratory for Computer Science and the MIT Artificial Intelligence Laboratory, both of which grew out of the original Project MAC. Leading researchers from the faculties and staffs of the laboratories highlight current research and future activities in multiprocessors and parallel computer architectures, in languages and systems for distributed computing, in intelligent systems (AI) and robotics, in complexity and learning theory, in software methodology, in programming language theory, in software for engineering research and education, and in the relation between computers and economic productivity.

    Contributors Abelson, Arvind, Rodney Brooks, David Clark, Fernando Corbato, William Daily, Michael Dertouzos, John Guttag, Berthold K. P. Horn, Barbara Liskov, Albert Meyer, Nicholas Negroponte, Marc Raibert, Ronald Rivest, Michael Sipser, Gerald Sussman, Peter Szolovits, and John Updike

    • Hardcover $57.00

Contributor

  • Dynamic Logic

    Dynamic Logic

    David Harel, Dexter Kozen, and Jerzy Tiuryn

    This book provides the first comprehensive introduction to Dynamic Logic.

    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. Dynamic Logic is a system of remarkable unity that is theoretically rich as well as of practical value. It can be used for formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other uses include determining the equivalence of programs, comparing the expressive power of various programming constructs, and synthesizing programs from specifications.

    This book provides the first comprehensive introduction to Dynamic Logic. It is divided into three parts. The first part reviews the appropriate fundamental concepts of logic and computability theory and can stand alone as an introduction to these topics. The second part discusses PDL and its variants, and the third part discusses DL and its variants. Examples are provided throughout, and exercises and a short historical section are included at the end of each chapter.

    • Hardcover $60.00 £50.00
    • Paperback $55.00 £45.00
  • Proof, Language, and Interaction

    Proof, Language, and Interaction

    Essays in Honour of Robin Milner

    Gordon Plotkin, Colin P. Stirling, and Mads Tofte

    This collection of original essays reflects the breadth of current research in computer science.

    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.

    Contributors Samson Abramsky, J. C. M. Baeten, Sergey Berezin, J. A. Bergstra, Gérard Berry, Lars Birkedal, Gérard Boudol, Edmund Clarke, Pierre Collette, Robert L. Constable, Pierre-Louis Curien, Jaco de Bakker, Uffe H. Engberg, William Ferreira, Fabio Gadducci, Mike Gordon, Robert Harper, Matthew Hennessy, Yoram Hirshfeld, C. A. R. Hoare, Gérard Huet, Paul B. Jackson, Alan S. A. Jeffrey, Somesh Jha, He Jifeng, Cliff B. Jones, Cosimo Laneve, Xinxin Liu, Will Marrero, Faron Moller, Ugo Montanari, Pavel Naumov, Mogens Nielsen, Joachim Parrow, Lawrence C. Paulson, Benjamin C. Pierce, Gordon Plotkin, M. A. Reniers, Amokrane Saïbi, Augusto Sampaio, Davide Sangiorgi, Scott A. Smolka, Eugene W. Stark, Christopher Stone, Mads Tofte, David N. Turner, Juan Uribe, Franck van Breugel, David Walker, Glynn Winskel

    • Hardcover $17.75 £14.99
  • Computability and Complexity

    Computability and Complexity

    From a Programming Perspective

    Neil Deaton Jones

    Computability and complexity theory should be of central concern to practitioners as well as theorists. Unfortunately, however, the field is known for its impenetrability. Neil Jones's goal as an educator and author is to build a bridge between computability and complexity theory and other areas of computer science, especially programming. In a shift away from the Turing machine- and Gödel number-oriented classical approaches, Jones uses concepts familiar from programming languages to make computability and complexity more accessible to computer scientists and more applicable to practical programming problems.

    According to Jones, the fields of computability and complexity theory, as well as programming languages and semantics, have a great deal to offer each other. Computability and complexity theory have a breadth, depth, and generality not often seen in programming languages. The programming language community, meanwhile, has a firm grasp of algorithm design, presentation, and implementation. In addition, programming languages sometimes provide computational models that are more realistic in certain crucial aspects than traditional models.

    New results in the book include a proof that constant time factors do matter for its programming-oriented model of computation. (In contrast, Turing machines have a counterintuitive "constant speedup" property: that almost any program can be made to run faster, by any amount. Its proof involves techniques irrelevant to practice.) Further results include simple characterizations in programming terms of the central complexity classes PTIME and LOGSPACE, and a new approach to complete problems for NLOGSPACE, PTIME, NPTIME, and PSPACE, uniformly based on Boolean programs.

    Foundations of Computing series

    • Hardcover $80.00 £65.00
  • Foundations for Programming Languages

    Foundations for Programming Languages

    John C. Mitchell

    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. Compared to other texts on the subject, Foundations for Programming Languages is distinguished primarily by its inclusion of material on universal algebra and algebraic data types, imperative languages and Floyd-Hoare logic, and advanced chapters on polymorphism and modules, subtyping and object-oriented concepts, and type inference. The book is mathematically oriented but includes discussion, motivation, and examples that make the material accessible to students specializing in software systems, theoretical computer science, or mathematical logic. Foundations for Programming Languages is suitable as a reference for professionals concerned with programming languages, software validation or verification, and programming, including those working with software modules or object-oriented programming.Foundations of Computing series

    • Hardcover $19.75 £15.99
  • Algorithmic Number Theory, Volume 1

    Algorithmic Number Theory, Volume 1

    Efficient Algorithms

    Eric Bach and Jeffrey Shallit

    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.

    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. Finally, it successfully blends computational theory with practice by covering some of the practical aspects of algorithm implementations. The subject of algorithmic number theory represents the marriage of number theory with the theory of computational complexity. It may be briefly defined as finding integer solutions to equations, or proving their non-existence, making efficient use of resources such as time and space. Implicit in this definition is the question of how to efficiently represent the objects in question on a computer. The problems of algorithmic number theory are important both for their intrinsic mathematical interest and their application to random number generation, codes for reliable and secure information transmission, computer algebra, and other areas. Publisher's Note: Volume 2 was not written. Volume 1 is, therefore, a stand-alone publication.

    • Hardcover $90.00 £75.00
    • Paperback $95.00 £78.00
  • Algebraic Semantics of Imperative Programs

    Algebraic Semantics of Imperative Programs

    Joseph A. Goguen and Grant Malcolm

    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. OBJ was designed for algebraic semantics; its declarations introduce symbols for sorts and functions, its statements are equations, and its computations are equational proofs. Thus, an OBJ "program" is an equational theory, and every OBJ computation proves some theorem about such a theory. This means that an OBJ program used for defining the semantics of a program already has a precise mathematical meaning. Moreover, standard techniques for mechanizing equational reasoning can be used for verifying axioms that describe the effect of imperative programs on abstract machines. These axioms can then be used in mechanical proofs of properties of programs. Intended for advanced undergraduates or beginning graduate students, Algebraic Semantics of Imperative Programs contains many examples and exercises in program verification, all of which can be done in OBJ.

    • Hardcover $10.75 £8.99
  • Circuit Complexity and Neural Networks

    Circuit Complexity and Neural Networks

    Ian Parberry

    Neural networks usually work adequately on small problems but can run into trouble when they are scaled up to problems involving large amounts of input data. Circuit Complexity and Neural Networks addresses the important question of how well neural networks scale - that is, how fast the computation time and number of neurons grow as the problem size increases. It surveys recent research in circuit complexity (a robust branch of theoretical computer science) and applies this work to a theoretical understanding of the problem of scalability. Most research in neural networks focuses on learning, yet it is important to understand the physical limitations of the network before the resources needed to solve a certain problem can be calculated. One of the aims of this book is to compare the complexity of neural networks and the complexity of conventional computers, looking at the computational ability and resources (neurons and time) that are a necessary part of the foundations of neural network learning. Circuit Complexity and Neural Networks contains a significant amount of background material on conventional complexity theory that will enable neural network scientists to learn about how complexity theory applies to their discipline, and allow complexity theorists to see how their discipline applies to neural networks.

    • Hardcover $12.75 £10.99
    • Paperback $50.00 £40.00
  • Theoretical Aspects of Object-Oriented Programming

    Theoretical Aspects of Object-Oriented Programming

    Types, Semantics, and Language Design

    Carl A. Gunter and John C. Mitchell

    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.

    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 fifteen chapters are divided into five parts: Objects and Subtypes, Type Inference, Coherence, Record Calculi, and Inheritance. The chapters are organized approximately in order of increasing complexity of the programming language constructs they consider - beginning with variations on Pascal- and Algol-like languages, developing the theory of illustrative record object models, and concluding with research directions for building a more comprehensive theory of object-oriented programming languages. Part I discusses the similarities and differences between "objects" and algebraic-style abstract data types, and the fundamental concept of a subtype. Parts II-IV are concerned with the "record model" of object-oriented languages. Specifically, these chapters discuss static and dynamic semantics of languages with simple object models that include a type or class hierarchy but do not explicitly provide what is often called dynamic binding. Part V considers extensions and modifications to record object models, moving closer to the full complexity of practical object-oriented languages.

    • Hardcover $75.00 £62.00
    • Paperback $40.00 £32.00
  • Logic and Information Flow

    Logic and Information Flow

    Jan van Eijck and Albert Visser

    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 logic of information flow has applications in both computer science and natural language processing and is a growing area within mathematical and philosophical logic. Consequently, Logic and Information Flow will be of interest to theoretical computer scientists wanting information on up-to-date formalisms of dynamic logic, and their possible applications; logicians who wish to expand their discipline beyond the realm of sound reasoning in the narrow sense; and philosophers who are looking at the nature of information and action, and at the relation between those concepts. Foundations of Computing series

    • Hardcover $11.75 £9.99
  • The Structure of Typed Programming Languages

    The Structure of Typed Programming Languages

    David A. Schmidt

    The text is unique in its tutorial presentation of higher-order lambda calculus and intuitionistic type theory.

    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. Using classical and recent research from lambda calculus and type theory, it presents a rational reconstruction of the Algol-like imperative languages such as Pascal, Ada, and Modula-3, and the higher-order functional languages such as Scheme and ML.David Schmidt's text is based on the premise that although few programmers ever actually design a programming language, it is important for them to understand the structuring techniques. His use of these techniques in a reconstruction of existing programming languages and in the design of new ones allows programmers and would-be programmers to see why existing languages are structured the way they are and how new languages can be built using variations on standard themes.The text is unique in its tutorial presentation of higher-order lambda calculus and intuitionistic type theory. The latter in particular reveals that a programming language is a logic in which its typing system defines the propositions of the logic and its well-typed programs constitute the proofs of the propositions. The Structure of Typed Programming Languages is designed for use in a first or second course on principles of programming languages. It assumes a basic knowledge of programming languages and mathematics equivalent to a course based on books such as Friedman, Wand, and Haynes': Essentials of Programming Languages. As Schmidt covers both the syntax and the semantics of programming languages, his text provides a perfect precursor to a more formal presentation of programming language semantics such as Gunter's Semantics of Programming Languages.

    • Hardcover $80.00
    • Paperback $9.75 £7.99
  • From Logic to Logic Programming

    From Logic to Logic Programming

    Kees Doets

    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. Advanced topics such as recursive complexity and negation as failure and its semantics are covered, and streamlined setups for SLD- and SLDNF-resolution are described. No other book treats this material in such detail and with such sophistication. Doets provides a novel approach to resolution that is applied to the first-order case and the case of (positive) logic programs. In contrast to the usual approach, the concept of a resolvent is defined nonconstructively, without recourse to the concept of unification, allowing the soundness and completeness proofs to be carried out in a more economic way. Other new material includes computability results dealing with analytical hierarchy, results on infinite derivations and an exposition on general logic programs using 3-valued logic.

    • Hardcover $10.75 £8.99
  • Exploring Interior-Point Linear Programming

    Exploring Interior-Point Linear Programming

    Algorithms and Software

    Ami Arbel

    This book provides practitioners as well as students of this general methodology with an easily accessible introduction to the new class of algorithms known as interior-point methods for linear programming.

    Linear programming is widely used in industry to solve complex planning and resource allocation problems. This book provides practitioners as well as students of this general methodology with an easily accessible introduction to the new class of algorithms known as interior-point methods for linear programming. In addition to presenting the theoretical and algorithmic background necessary for dealing with specific interior-point linear programming algorithms, it offers a review of modeling linear programming problems, a review of the simplex algorithm that has been used to solve linear programming problems in the past, and a complete user's guide to the software that is included with the book.The interior-point technique is proving especially powerful for the solution of large-scale linear programming problems, with better performance bounds than the simplex algorithm. For example, the U.S. Military airlift command has solved their scheduling problem using interior-point algorithms much faster and with a longer planning horizon than was possible with the simplex algorithms, and Delta expects to save millions of dollars by using interior-point methods to schedule their air crews and planes.The software package is designed for use on IBM-PC microcomputers (and compatibles), a platform that provides an ideal environment for students of linear programming interested in exploring and studying these new algorithms.Contents: Preparations. Introduction. Modeling Linear Optimization Problems. The Simplex Algorithm. A First Look at an Interior Point Algorithm. Algorithms. The Primal Algorithm. The Dual Algorithm. The Primal-Dual Algorithm. Implementation Issues. Solutions. The Integrated Environment. Command Line Operations. Appendixes.

    • Paperback $45.00 £38.00
  • Hilbert's 10th Problem

    Hilbert's 10th Problem

    Yuri Matiyasevich

    This book presents the full, self-contained negative solution of Hilbert's 10th problem.

    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.This book presents the full, self-contained negative solution of Hilbert's 10th problem. In addition it contains a number of diverse, often striking applications of the technique developed for that solution (scattered previously in journals), describes the many improvements and modifications of the original proof - since the problem was "unsolved" 20 years ago, and adds several new, previously unpublished proofs. Included are numerous exercises that range in difficulty from the elementary to small research problems, open questions, and unsolved problems. Each chapter concludes with a commentary providing a historical view of its contents. And an extensive bibliography contains references to all of the main publications directed to the negative solution of Hilbert's 10th problem as well as the majority of the publications dealing with applications of the solution. Intended for young mathematicians, Hilbert's 10th Problem requires only a modest mathematical background. A few less well known number-theoretical results are presented in the appendixes. No knowledge of recursion theory is presupposed. All necessary notions are introduced and defined in the book, making it suitable for the first acquaintance with this fascinating subject.

    • Hardcover $55.00 £45.00
  • The Formal Semantics of Programming Languages

    The Formal Semantics of Programming Languages

    An Introduction

    Glynn Winskel

    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.Starting with basic set theory, structural operational semantics is introduced as a way to define the meaning of programming languages along with associated proof techniques. Denotational and axiomatic semantics are illustrated on a simple language of while-programs, and fall proofs are given of the equivalence of the operational and denotational semantics and soundness and relative completeness of the axiomatic semantics. A proof of Godel's incompleteness theorem, which emphasizes the impossibility of achieving a fully complete axiomatic semantics, is included. It is supported by an appendix providing an introduction to the theory of computability based on while-programs. Following a presentation of domain theory, the semantics and methods of proof for several functional languages are treated. The simplest language is that of recursion equations with both call-by-value and call-by-name evaluation. This work is extended to lan guages with higher and recursive types, including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship between denotational and operational semantics is stressed, and the proofs of the correspondence between the operation and denotational semantics are provided. The treatment of recursive types - one of the more advanced parts of the book - relies on the use of information systems to represent domains. The book concludes with a chapter on parallel programming languages, accompanied by a discussion of methods for specifying and verifying nondeterministic and parallel programs.

    • Hardcover $50.00 £40.00
    • Paperback $70.00 £58.00
  • Semantics of Programming Languages

    Semantics of Programming Languages

    Structures and Techniques

    Carl A. Gunter

    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.

    • Hardcover $115.00 £95.00
    • Paperback $45.00 £38.00
  • Basic Category Theory for Computer Scientists

    Basic Category Theory for Computer Scientists

    Benjamin C. Pierce

    Basic Category Theory for Computer Scientists provides a straightforward presentation of the basic constructions and terminology of category theory, including limits, functors, natural transformations, adjoints, and cartesian closed categories.

    Category theory is a branch of pure mathematics that is becoming an increasingly important tool in theoretical computer science, especially in programming language semantics, domain theory, and concurrency, where it is already a standard language of discourse. Assuming a minimum of mathematical preparation, Basic Category Theory for Computer Scientists provides a straightforward presentation of the basic constructions and terminology of category theory, including limits, functors, natural transformations, adjoints, and cartesian closed categories. Four case studies illustrate applications of category theory to programming language design, semantics, and the solution of recursive domain equations. A brief literature survey offers suggestions for further study in more advanced texts.

    Contents Tutorial • Applications • Further Reading

    • Paperback $35.00 £28.00
  • Single-Layer Wire Routing and Compaction

    F. Miller Maley

    This pioneering study of two-dimensional wiring patterns develops powerful algorithms for the physical design of VLSI circuits. Its homotopic approach to circuit layout advances the state of the art in wire routing and layout compaction, and will inspire future research. By viewing wires as flexible connections with fixed topology, the author obtains simple and efficient algorithms for CAD problems whose previous solutions employed, unreliable or inefficient heuristics.Single-Layer Wire Routing and Compaction is the first rigorous treatment of homotopic layouts and the techniques for optimizing them. In a novel application of classical mathematics to computer science, Maley characterizes the ideal routing of a layout in terms of simple topological invariants. He derives practical algorithms from this theoretical insight. The algorithms and their underlying ideas are intuitive, widely applicable, and presented in a highly readable style.

    Single-Layer Wire Routing and Compaction is included in the series Foundations of Computing, edited by Michael Garey and Albert Meyer.

    • Hardcover $45.00
  • The Stable Marriage Problem

    The Stable Marriage Problem

    Structure and Algorithms

    Dan Gusfield and Robert W. Irving

    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.The authors develop the structure of the set of stable matchings in the stable marriage problem in a more general and algebraic context than has been done previously; they discuss the problem's structure in terms of rings of sets, which allows many of the most useful features to be seen as features of a more general set of problems. The relationship between the structure of the stable marriage problem and the more general stable roommates problem is demonstrated, revealing many commonalities.The results the authors obtain provide an algorithmic response to the practical, and political, problems created by the asymmetry inherent in the Gale Shapley solutions, leading to alternative methods and better compromises than are provided by the Gale Shapley method. And, in contrast to Donald Knuth's earlier work which primarily focused on the application of mathematics to the analysis of algorithms, this book illustrates the productive and almost inseparable relationship between mathematical insight and the design of efficient algorithms.

    The Stable Marriage Problem is included in the Foundations of Computing Series, edited by Michael Garey and Albert Meyer.

    • Hardcover $45.00
    • Paperback $25.00 £20.00
  • Realistic Compiler Generation

    Peter Lee

    In this book Peter Lee provides a complete description and survey of the field of semantics based compiler generation and presents a new method for expressing the formal semantics of programming languages that allows realistic compilers to be generated automatically. The method Lee describes has two main advantages over previous methods. First, it allows compilers to be generated automatically. The compilers are realistic in the sense that they compile programs as efficiently as hand crafted compilers do, and the object programs they produce run as efficiently as the object programs produced by hand crafted compilers. The second advantage is that it makes it easier to comprehend and write the semantics than other methods.The book demonstrates a working compiler generator called MESS which is used to generate a realistic compiler for a Pascal-like language. The generated compiler is then compared with several hand crafted compilers and shown to have at least comparable, and in some cases superior, performance.

    Realistic Compiler Generation is included in the series Foundations of Computing, edited by Michael Garey and Albert Meyer.

    • Hardcover $32.50
  • PX

    A Computational Logic

    Susumu Hayashi and Hiroshi Nakano

    The computational logic PX (Program eXtractor) is used to verify programs, extract programs from constructive proofs, and give foundations to type theories. While it is well known theoretically that programs can be extracted from constructive proofs, this study shows how it can be done in practice. The authors give a precise description of the formal theory of PX, its semantics, the mathematical foundation of program extraction using PX, and several methodologies and their theories of program extraction. They also describe an experimental implementation of PX.

    Contents Introduction • Formal System • Realizability • Writing Programs via proofs • PX as a foundation of type theories • Semantics • Implementing PX

    PX: A Computational Logic is included in the Foundations of Computing series edited by Michael Garey and Albert Meyer.

    • Hardcover $32.95 £28.00
  • Resource Allocation Problems

    Algorithmic Approaches

    Toshihide Ibaraki and Naoki Katoh

    This book addresses a theoretical problem encountered in a variety of areas in operations research and management science, including load distribution, production planning, computer scheduling, portfolio selection, and apportionment. It is a timely and comprehensive summary of the past thirty years of research on algorithmic aspects of the resource allocation problem and its variants, covering Lagrangean multiplier method, dynamic programming, greedy algorithms, and their generalizations. Modern data structures are used to analyze the computational complexity of each algorithm.The resource allocation problem the authors take up is an optimization problem with a single simple constraint: it determines the allocation of a fixed amount of resources to a given number of activities in order to achieve the most effective results. It may be viewed as a special case of the nonlinear programming or nonlinear integer programming problem.

    Contents Introduction • Resource Allocation with Continuous Variables • Resource Allocation with Integer Variables • Minimizing a Convex Separable Function • Minimax and Maximin Resource Allocation Problems • Fair Resource Allocation Problem • Apportionment Problem • Fundamentals of Submodular Systems • Resource Allocation Problems under Submodular Constraints • Further Topics on Resource Allocation Problems • Appendixes: Algorithms and Complexity • NP-completeness and NP-hardness

    Resource Allocation Problems is included in the Foundations of Computing Series edited by Michael Garey and Albert Meyer.

    • Hardcover $49.95
  • Theory of Deductive Systems and Its Applications

    S. Yu. Maslov

    In a fluent, clear, and lively style this translation by two of Maslov's junior colleagues brings the work of the late Soviet scientist S. Yu. Maslov to a wider audience. Maslov was considered by his peers to be a man of genius who was making fundamental contributions in the fields of automatic theorem proving and computational logic. He published little, and those few papers were regarded as notoriously difficult. This book, however, was written for a broad audience of readers and describes elegant examples of applications in such fields as computer science, artificial intelligence, operations research, economic modeling, and biological modeling, among others. The book also brings to light the work by the American mathematician E. L. Post, which inspired Maslov's own work in the development of a general theory and which has been long neglected by mathematicial logicians and systems theorists in the United States. The book's first chapter introduces the Rules of the Game. Part I, Mathematics of Calculi, covers E. L. Post's canonical systems, deductive systems and algorithms, and probabilistic calculi and deductive information. Part II, Horizonal Modeling, takes up a "toy" economy, the calculi of technological possibilities, and the development of rules. Part III, Vertical Modeling, deals with the topics of "to fight and to search" and the consequences of the asymmetry of cognitive mechanisms.

    Theory of Deductive Systems and Its Applications is included in the Foundation of Computing Series, edited by Michael Garey.

    • Hardcover $27.95
  • Equational Logic as a Programming Language

    Michael J. O'Donnell

    This book provides a comprehensive description of the theoretical foundations, design, and implementation of an innovative logic programming language in which computations are produced directly from equational definitions. Like LISP and Prolog, the equational programming language is based on the concept that a programmer should give a mathematical description of the result of a computation rather than a series of commands to direct a computation. Unlike LISP and Prolog, however, the equational programming language strictly follows the rules of equational logic, providing powerful programming techniques not available in conventional languages. Equational Logic as a Programming Language covers the entire spectrum of theoretical and applied work involved in eight years of designing and implementing the equational logic programming language. Separate chapters cover the intuitive logical semantics of the language, the powerful programming techniques supported by it and their connections to procedural techniques such as coroutines, the methods used to produce a highly flexible implementation of the language with very little manpower, and the potential for implementation on parallel computers.

    Equational Logic as a Programming Language is included in the Foundations of Computing Series, edited by Michael Garey.

    • Hardcover $49.95
  • Complexity Issues in VLSI

    Complexity Issues in VLSI

    Optimal Layouts for the Shuffle-Exchange Graph and Other Networks

    Frank Thomson Leighton

    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. The mesh of trees network (which may eventually prove as useful as the shuffle-exchange graph) is introduced and the book shows how it can be used to perform a variety of computations, including sorting and matrix multiplication, in a logarithmic number of steps. Next, the book introduces the tree of meshes, the first planar graph that was discovered not to have a linear-area layout. Most recently, the structure of this graph has been used to develop a general framework for solving VLSI graph layout problems. Finally, the book develops techniques for proving lower bounds on the bisection width, crossing number, and layout area of a graph. These techniques significantly extend the power and range of previous methods.Researchers in the fields of VLSI, parallel computation, and graph theory will find this study of particular value; it is also accessible to anyone with an elementary knowledge of mathematics and computer science. The book is self-contained and presents in a unified and original manner many results scattered in the technical literature, while also covering new and fundamental results for the first time.

    • Hardcover $27.50
    • Paperback $25.00 £20.00