Algebraic Approaches to Program Semantics

1. Front Matter

   Pages i-xi

   PDF

2. Denotational Semantics of Control

   1. Front Matter

      Pages 1-1

      PDF

   2. An Introduction to Denotational Semantics

      • Ernest G. Manes, Michael A. Arbib

      Pages 3-37

   3. An Introduction to Category Theory

      • Ernest G. Manes, Michael A. Arbib

      Pages 38-70

   4. Partially Additive Semantics

      • Ernest G. Manes, Michael A. Arbib

      Pages 71-97

   5. Assertion Semantics

      • Ernest G. Manes, Michael A. Arbib

      Pages 98-115

3. Semantics of Recursion

   1. Front Matter

      Pages 117-117

      PDF

   2. Recursive Specifications

      • Ernest G. Manes, Michael A. Arbib

      Pages 119-145

   3. Order Semantics of Recursion

      • Ernest G. Manes, Michael A. Arbib

      Pages 146-175

   4. Canonical Fixed Points

      • Ernest G. Manes, Michael A. Arbib

      Pages 176-179

   5. Partially Additive Semantics of Recursion

      • Ernest G. Manes, Michael A. Arbib

      Pages 180-209

   6. Fixed Points in Metric Spaces

      • Ernest G. Manes, Michael A. Arbib

      Pages 210-231

4. Data Types

   1. Front Matter

      Pages 233-233

      PDF

   2. Functors

      • Ernest G. Manes, Michael A. Arbib

      Pages 235-257

   3. Recursive Specification of Data Types

      • Ernest G. Manes, Michael A. Arbib

      Pages 258-278

   4. Parametric Specification

      • Ernest G. Manes, Michael A. Arbib

      Pages 279-292

   5. Order Semantics of Data Types

      • Ernest G. Manes, Michael A. Arbib

      Pages 293-317

   6. Equational Specification

      • Ernest G. Manes, Michael A. Arbib

      Pages 318-340

5. Back Matter

   Pages 341-353

   PDF

In the 1930s, mathematical logicians studied the notion of "effective comput­ ability" using such notions as recursive functions, A-calculus, and Turing machines. The 1940s saw the construction of the first electronic computers, and the next 20 years saw the evolution of higher-level programming languages in which programs could be written in a convenient fashion independent (thanks to compilers and interpreters) of the architecture of any specific machine. The development of such languages led in turn to the general analysis of questions of syntax, structuring strings of symbols which could count as legal programs, and semantics, determining the "meaning" of a program, for example, as the function it computes in transforming input data to output results. An important approach to semantics, pioneered by Floyd, Hoare, and Wirth, is called assertion semantics: given a specification of which assertions (preconditions) on input data should guarantee that the results satisfy desired assertions (postconditions) on output data, one seeks a logical proof that the program satisfies its specification. An alternative approach, pioneered by Scott and Strachey, is called denotational semantics: it offers algebraic techniques for characterizing the denotation of (i. e. , the function computed by) a program-the properties of the program can then be checked by direct comparison of the denotation with the specification. This book is an introduction to denotational semantics. More specifically, we introduce the reader to two approaches to denotational semantics: the order semantics of Scott and Strachey and our own partially additive semantics.

• Boolean algebra
• computer
• control
• evolution
• formal language
• formal languages
• functional programming
• mathematical logic
• program semantics
• programming
• programming language
• proof
• proving
• semantics

• Department of Mathematics and Statistics, University of Massachusetts, Amherst, USA

  Ernest G. Manes

• Departments of Computer Science, Neurobiology and Physiology, University of Southern California, Los Angeles, USA

  Michael A. Arbib

Policies and ethics