Book contents
- Frontmatter
- Contents
- List of Contributors
- Preface
- Semantics of Interaction: an Introduction to Game Semantics
- Computational Content of Classical Logic Thierry Coquand
- Syntax and Semantics of Dependent Types
- Game Semantics
- Metalanguages and Applications
- Operationally-Based Theories of Program Equivalence
- Categories in Concurrency
- Index
Semantics of Interaction: an Introduction to Game Semantics
Published online by Cambridge University Press: 15 September 2009
- Frontmatter
- Contents
- List of Contributors
- Preface
- Semantics of Interaction: an Introduction to Game Semantics
- Computational Content of Classical Logic Thierry Coquand
- Syntax and Semantics of Dependent Types
- Game Semantics
- Metalanguages and Applications
- Operationally-Based Theories of Program Equivalence
- Categories in Concurrency
- Index
Summary
Introduction
The “classical” paradigm for denotational semantics models data types as domains, i.e. structured sets of some kind, and programs as (suitable) functions between domains. The semantic universe in which the denotational modelling is carried out is thus a category with domains as objects, functions as morphisms, and composition of morphisms given by function composition. A sharp distinction is then drawn between denotational and operational semantics. Denotational semantics is often referred to as “mathematical semantics” because it exhibits a high degree of mathematical structure; this is in part achieved by the fact that denotational semantics abstracts away from the dynamics of computation—from time. By contrast, operational semantics is formulated in terms of the syntax of the language being modelled; it is highly intensional in character; and it is capable of expressing the dynamical aspects of computation.
The classical denotational paradigm has been very successful, but has some definite limitations. Firstly, fine-structural features of computation, such as sequentially, computational complexity, and optimality of reduction strategies, have either not been captured at all denotationally, or not in a fully satisfactory fashion. Moreover, once languages with features beyond the purely functional are considered, the appropriateness of modelling programs by functions is increasingly open to question. Neither concurrency nor “advanced” imperative features such as local references have been captured denotationally in a fully convincing fashion.
- Type
- Chapter
- Information
- Semantics and Logics of Computation , pp. 1 - 32Publisher: Cambridge University PressPrint publication year: 1997
- 29
- Cited by