SEMANTIC STRUCTURES
HANDBOOK OF LOGIC IN COMPUTER SCIENCE(Vol.3)
by
ABRAMSKY, GABBAY and MAIBAUM
DOMAIN THEORY
Introduction and Over View
- Origins
- Our Approach
- Overview
Domains individually
- Convergence
- Approximation
- Topology
Domains Collectively
- Comparing domains
- Finitary constructions
- Infinitary constructions
Cartesian closed categories of domains
- Local uniqueness: Lattice-like domains
- Finite choice: Compact domains
- The hierarchy of categories of domains
Recursive domain equations
- Examples
- Construction of solutions
- Canonicity
- Analysis of solutions
Equational Theories
- General techniques
- Powderdomains
Domains and logic
- Stone Duality
- Some equivalences
- The logical viewpoint
Further directions
- Further topics in 'classical domain theory'
- Stability and sequentiality
- Reformulations of domain theory
- Axiomatic domain theory
- Syntheitic domain theory
Guide to the Literature
DENOTATIONAL SEMANTICS
Introduction
- Approaches
- An example: binary numerals
- Compositionality
- Criteria
- Overview
- Bibliographic notes
A simple imperative language
- Expressions and commands
- Assignment commands
- Indefinite iterations
- Programs
- Operational semantics
- Programming logic
- Non-determination
- Bibliographic notes
A simple applicative language
- Definitions and function applications
- Function definitions
- Defined notation
- Elementary properties
- Programming logic
- Bibliographic notes
Recursion
- Recursive definitions
- Domain-theoretic semantics
- Programming logic
- Full abstraction
- Untyped procedures
- Bibliographic notes
An Algol-like language I
- Syntax
- Semantics
- Call by value
- Programming logic
- Bibliographic notes
An Algol-like language II
- Coercions
- Local variables
- Product types and arrays
- Lists
- Acceptors
- Jumps
- Intermediate output
- Block expressions
- Bibliographic notes
Possible worlds
- Functor category semantics
- Semantic-domain functors
- Semantic valuations
- Semantics of local variables
- Specifications
- Non-interference specifications
- Semantics of block expressions
- Bibliographic notes
ALGEBRAIC SEMANTICS
Introduction and motivation
- General remarks
- Some motivating examples
- A notational 'crisis'
Algebraic theories, definitions and examples
- General remarks
- Basic definitions
- Algebraic theories as categories
- Examples of algebraic theories
- Notations and basic identities
Ordered theories
- Definition of ordered and continuous theories
- Examples of ordered theories
Theories with iteration operators
- Iteration operators
- Iteration, rational, and iterative theories
- The lambda-operator
- Iteration operators and flowcharts
- Interpretations of flowcharts
More about iteration operators
- Relationships between iteration, rational and iterative theories
- Some identities for iteration operators
Iteration closure, and normal form theorems
Free theories and Hebrand interpretations
- Free theories
- The general case
Recursive hierarchies
THE SEMANTICS OF TYPES IN PROGRAMMING LANGUAGES
Introduction
Types in programming
- Higher types
- Recursive types
- Parametric polymorphism
- Subtypes
Simple types as sets
- Types and equations
- Sets as a model
- Type frames
- Completeness for sets
Simple types as domains
- A programming language for computible functions
- Operational semantics
- Operational equivalence
- bc-domains and dI-domains
- Full abstraction
Types as invariants
- Run-time safety
- Implicit types
- Run-time safety for assignments and continuations
Types as subsets
- Untyped lambda-calculus
- What is a model of the untyped lambda-calculus
- What models of the untyped lambda-calculus are there?
- Inclusive subsets as types
- Subtyping as subset inclusion
Types as partial equivalence relations
- Sets as a model of ML0 types
- Another typing system for ML0
- The polymorphic lambda-calculus
- Sets as a model of polymorphic types?
- Simple types as PERs
- PERs as a model of polymorphic types
Conclusion
return
to
Mathematical Structures Group