[Prev][Next][Index][Thread]

book announcement "LOGIC OF DOMAINS"

Date:  Tue, 26 Nov 1991 10:40:47 -0500

                 --------------------
                   LOGIC OF DOMAINS
                 --------------------

                   by Guo-Qiang Zhang

Birkhauser, Boston.Basel.Berlin (Progress in Theoretical Computer Science)
1991, ISBN 0-8176-3570-X,  ISBN 3-7643-3570-X (259 pages)

Abstract: This monograph studies the logical aspects of domains as used
in denotational semantics of programming languages. Frameworks of domain
logics are introduced; these serve as foundations for systematic
derivations of proof systems from denotational semantics of programming 
languages. Any proof system so derived is guaranteed to agree with
denotational semantics in the sense that the denotation of any program
coincides with the set of assertions true of it. The study focuses on
two prominent categories for denotational semantics: SFP domains, and
the less standard, but important, category of stable domains.
  
The intended readership includes researchers and graduate students
interested in the relation between semantics of programming languages and
formal means of reasoning about programs.
  
     Table of Contents:

Part I  SFP domains

	1. Introduction 
           1.1 Domain theory
           1.2 Program Logics
           1.3 Logic and Topology
           1.4 Logic of Domains
	2. Prerequisites
           2.1 Cpos and Domains
           2.2 Constructions on Cpos
           2.3 Fixed-Point Theory
           2.4 Scott Topology
           2.5 SFP Domains
           2.6 Powerdomains
           2.7 Finite Elements
           2.8 Compact Open Stes
           2.9 Recursively Defined Domains
           2.10 More about SFP Domains
	3. A Representation of SFP
           3.1 Sequent Structures
           3.2 Information Systems
           3.3 Strongly Finite Sequent Structures
           3.4 A Category of SFSS
           3.5 Powerdomains
           3.6 A Cpo of SFSS
	4. A Logic of SFP
           4.1 Typed Assertion Languages
           4.2 Proof Systems       
           4.3 Soundness
           4.4 Completeness
           4.5 Pure Relative Completeness
           4.6 An Application
           4.7 Non-entailment
	5. A Mu-Calculus
           5.1 Recursive Assertions
           5.2 Theorems
           5.3 Two Special Rules
           5.4 Soundness and Completeness
           5.5 The Definable Subsets of N_{\bot}

Part II Stable Domains
	
	6. Categories
           6.1 Cartesian Closed Categories
           6.2 Categories for Concurrency
           6.3 Monoidal Closed Categories
           6.4 Relationships among the Categories
	7. A Representation of DI
           7.1 Prime Information Systems
           7.2 A Category of PIS
           7.3 A Cpo of PIS
           7.4 Constructions
           7.5 Coherent Information Systems
	8. Stable Neighborhoods
           8.1 Stable Neighborhoods
           8.2 Constructions in DI
           8.3 Constructions in COH
           8.4 Parallel Products
	9. Disjunctive Logics
           9.1 Disjunctive Assertions
           9.2 Completeness and Expressiveness
           9.3 The Logic of DI
           9.4 Completeness
           9.5 An Alternative Approach
	10. Research Topics
        Bibliography
        Index