Technical Reports

The ICICS/CS Reading Room

UBC CS TR-91-31 Summary

Solving Domain Equations in NaDSet, December 1991 Paul C. Gilmore and George K. Tsiknis, 23 pages

Solutions of systems of domain equations is the basis for what is called the Strachey-Scott approach to providing a denotational semantics for programming languages. The solutions offered by the mathematical methods developed by Scott, however, do not provide a computational basis for the semantics in the form of a proof theory. The purpose of this paper is to provide such a theory using the logic and set theory NaDSet. \nThe development of NaDSet was motivated by the following three principles:\\ 1. Abstraction, along with truth functions and quantification, is one of the three fundamental concepts of logic and should be formalized in the same manner as the other two.\\ 2. Natural deduction presentations of logic provide a transparent formalization of Tarski's reductionist semantics.\\ 3. Atomic formulas receive their truth values from a nominalist interpretation. \nThat these three principles lead to a successful resolution of the set theoretic paradoxes and to a sound formulation of NaDSet has been demonstrated elsewhere with proofs of consistency and completeness. Applications of NaDSet to programming language semantics, category theory, non-well-founded sets, and to foundational questions of mathematics have also been demonstrated. \nThe financial support of the Natural Science and Engineering Research Council of Canada is gratefully acknowledged.

If you have any questions or comments regarding this page please send mail to