The logical aspects of semantic domains used in the formal definition of programming languages are investigated. This book provides a complete overview of domain theory and generates logical frameworks to link denotational semantics and program logics (such as axiomatic semantics). It constructs the basis for determining the equivalence between denotational and axiomatic semantics, a notion quite similar to full abstraction in the context of denotational and operational semantics. Even though no discontinuity occurs, the book is divided into two parts. The first part deals with the category of sequence of finite inductive partial orders (SFP) domains, while the second part deals with the category of stable domains.
Chapter 1 provides an overview of several topics related to formal semantics. Domain theory, program logics, and proof systems are described in some detail to provide an adequate basis for subsequent chapters. The connection between denotational semantics and program logics is shown to be related to topological ideas. The last part of the chapter gives a useful summary of the remaining chapters.
Chapter 2 is a concise introduction to the general theory of domains. Known results in domain theory are presented, and proofs of major theorems are developed. Zhang reviews domain and power domain constructions and their Scott topology. A new characterization of finite elements of the function space for SFP domains is given.
Chapter 3 introduces sequent structures, which are structures derived from Gentzen’s sequent calculus. Deterministic sequent structures are shown to correspond to information systems. This correspondence defines the logic of domains constructed from sequent structures. Another kind of sequent structure, the strongly finite sequent structure (SFSS), is defined and shown to be an SFP domain. A category of SFSSs is constructed from SFSSs as objects and approximable mappings as morphisms. This category is equivalent to the category of SFP domains. Power domain constructions are defined on SFSSs.
Chapter 4 defines a logic of SFP domains. A nice, powerful property of the resulting logical framework is the formal derivation of a sound and complete proof system of a programming language from its denotational semantics. That is, an axiomatic semantics can be formally derived from its equivalent denotational semantics. This framework consists of a metalanguage for denotational semantics, a set of typed assertion languages, a set of structural and logical rules, and a set of metapredicates. The soundness, completeness, and expressiveness of the associated proof system are proven.
Chapter 5 studies &mgr;-calculus, an extension of the assertion language introduced in the previous chapter. The least fixed-point construct is added to augment the expressive power of the language. Zhang gives a proof system for &mgr;-calculus and demonstrates its soundness. Completeness is also shown for the &mgr;-calculus of integers.
Chapter 6 provides background for the second part of the book. Several categories of coherent spaces, stable domains, and event structures are presented, and the relationships among them are discussed.
Chapter 7 introduces prime information systems as a representation of dI-domains. The categories of prime information systems and dI-domains are shown to be equivalent. Constructions (lifting, sum, product, function space) are developed. A complete partial order of prime information systems is constructed to support recursive definitions of these systems using fixed point theory.
Chapter 8 investigates stable neighborhoods. A new topology, different from the Scott topology, is developed to characterize stable domains. The author develops constructions (sum, lift, product, tensor product, function space) and introduces other constructions in the category of coherent spaces (linear function space and exponential). These constructions are shown to preserve compactness.
Chapter 9 studies two approaches to the logic of stable domains. The first approach is based on a disjunctive assertion language, while the second is based on a conventional assertion language. Consequently, two logical frameworks, COHl for coherent spaces with linear stable functions and DI for dI-domains with stable functions, are developed. Proof systems are introduced, and soundness, completeness, and expressiveness are discussed.
Chapter 10 provides a summary and a discussion of future research.
This book is a revised version of a Ph.D. dissertation. It is intended for researchers in formal semantics with a background in domain theory and familiarity with topology and category theory. It is well written and well organized, thus providing an incentive for reading difficult and highly technical material. Careful preparation and editing of the book add substantial value to the physical and technical presentation of the material. This book constitutes a fundamental contribution to the study of formal semantics of programming languages. The logical frameworks developed by the author provide a firm foundation for deriving program logics from denotational semantics.
