×

Domain theory in logical form. (English) Zbl 0737.03006

The article is a very interesting attempt to connect domain theory, logics of programs, and concurrency. The author moves in the mathematical framework of Stone duality. Up to now, Stone duality was important for topology and logic. The author points out its importance for computer science: Stone duality provides the framework for understanding the relationship between denotational semantics and program logics. A metalanguage with types and terms (programs) is introduced. A denotational interpretation, and then a logical one are given. The two interpretations are Stone duals of each other (“a strengthened form of the logician’s soundness and completeness”). Each determines the other up to isomorphism. Consequently, semantics and logic are guaranteed to be in harmony with each other. Finally, directions for further research are discussed. A deep and provocative paper. A very good reference article.
Reviewer: G.Ciobanu (Iaşi)

MSC:

03B70 Logic in computer science
68Q55 Semantics in the theory of computing
06E15 Stone spaces (Boolean spaces) and related structures
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abramsky, S., Semantic foundations for applicative multiprogramming, (), 1-14 · Zbl 0538.68064
[2] Abramsky, S., Domain theory and the logic of observable properties, Ph.D. thesis, (1987), Univ. London
[3] Abramsky, S.; Abramsky, S., Domain theory and the logic of observable properties, Information and computation, Ph.D. thesis, (1987), Univ. London, Chapter 5
[4] Abramsky, S., Domain theory in logical form, (), 47-53
[5] Abramsky, S.; Abramsky, S., Domain theory and the logix of observable properties, (), Ph.D. thesis, 65-117, (1987), Univ. London, Chapter 6
[6] S. Abramsky, Total vs. partial objects in denotational semantics, to appear.
[7] ()
[8] Aczel, P., An introduction to inductive definitions, ()
[9] Barendregt, H., The lambda calculus: its syntax and semantics, Studies in logic and the foundations of mathematics, 103, (1984), North-Holland Amsterdam · Zbl 0551.03007
[10] Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda model and the completeness of type-assignment, J. symbolic logic, 48, 931-940, (1983) · Zbl 0545.03004
[11] Barr, M.; Wells, C., Toposes, triples and theories, (1984), Springer Berlin · Zbl 0567.18001
[12] Barwise, J., An introduction to first order logic, (), 5-46
[13] Berry, G.; Curien, P.-L., Theory and practice of sequential algorithms: the kernel of the applicative language CDS, (), 35-84 · Zbl 0619.68008
[14] Berry, G.; Curien, P.-L.; Lévy, J.-J., Full abstraction for sequential languages: the state of the art, (), 89-132 · Zbl 0604.68033
[15] Chang, C.C.; Keisler, H.J., Model theory, Studies in logic and the foundations of mathematics, 73, (1977), North-Holland Amsterdam · Zbl 0697.03022
[16] Coppo, M.; Dezani-Ciancaglini, M.; Honsell, F.; Longo, G., Extended type structure and filter lambda models, (), 241-262 · Zbl 0558.03007
[17] Damas, L.; Milner, R., Principal type schemes for functional programs, (), 207-212
[18] de Bakker, J.W., Mathematical theory of program correctness, (1980), Prentice-Hall Englewood Cliffs, NJ
[19] de Bakker, J.W.; Zucker, J., Processes and the denotational semantics of concurrency, Inform. and control, 54, 70-120, (1982) · Zbl 0508.68011
[20] Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[21] Dugundji, J., Topology, (1966), Allyn & Bacon Newton, MA
[22] Egli, H.; Constable, R.L., Computability concepts for programming language semantics, Theoret. comput. sci., 2, 2, 133-145, (1976) · Zbl 0352.68042
[23] Ershov, Yu.L., Computable functionals of finite types, Algebra and logic, 11, 4, 367-437, (1972)
[24] Gierz, G.K.; Hoffman, K.H.; Keimel, K.; Lawson, J.D.; Mislove, M.; Scott, D.S., A compendium of continuous lattices, (1980), Springer Berlin · Zbl 0452.06001
[25] Girard, J.-Y., Linear logic, Theoret. comput. sci., 50, 1, 1-102, (1987) · Zbl 0625.03037
[26] Gordon, M.J.C., The denotational description of programming languages, (1979), Springer Berlin · Zbl 0425.68015
[27] Graf, S.; Sifakis, J., A logic for the specification and proof of regular controllable processes of CCS, Acta inform., 23, 507-527, (1986) · Zbl 0599.68025
[28] Gunter, C., Profinite solutions for recursive domain equations, Technical report CMU-CS-85-107, (1985), Carnegie-Mellon Univ.
[29] Gunter, C., The largest first-order axiomatizable Cartesian closed category of domains, (), 142-148
[30] Gunter, C., Universal profinite domains, Inform. and comput., 72, 1, 1-30, (1987) · Zbl 0628.68050
[31] Harel, D., First order dynamic logic, Lecture notes in comput. sci., 68, (1979), Springer Berlin · Zbl 0403.03024
[32] Hennessy, M.C.B.; Milner, R., Algebraic laws for non-determinism and concurrency, J. assoc. comput. mech., 32, 137-161, (1985) · Zbl 0629.68021
[33] Hennessy, M.C.B.; Plotkin, G.D.; Beçvar, J., Full abstraction for a simple parallel programming language, Mathematical foundations of computer science, lecture notes in comput. sci., 74, (1979), Springer Berlin · Zbl 0457.68006
[34] Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 576-580, (1969) · Zbl 0179.23105
[35] Hyland, J.M., Function spaces in the category of locales, (), 264-281 · Zbl 0483.54005
[36] Johnstone, P.T., Stone spaces, Cambridge stud. adv. math., 3, (1982), Cambridge Univ. Press Cambridge · Zbl 0499.54001
[37] Johnstone, P.T., Vietoris locales and localic semi-lattices, (), 155-180
[38] Kanda, A., Fully effective solutions of recursive domain equations, () · Zbl 0404.68008
[39] Kanda, A., Fully effective solutions of recursive domain equations, Ph.D. thesis, (1980), Univ. Warwick
[40] Kozen, D., A representation theorem for models of ★-free PDL, (), 351-362
[41] Kozen, D., On the duality of dynamic algebras and Kripke models, (), 1-11
[42] Kozen, D., A probabilistic PDL, (), 291-297
[43] Kreisel, G., Interpretation of analysis by means of functionals of finite type, ()
[44] Lambek, J.; Scott, P.J., Introduction to higher order categorial logic, Cambridge stud. adv. math., 7, (1986), Cambridge Univ. Press Cambridge · Zbl 0596.03002
[45] Larsen, K.G.; Winskel, G., Using information systems to solve recursive domain equations effectively, (), 109-130 · Zbl 0539.68019
[46] Lawvere, F.W., Metric spaces, generalized logic, and closed categories, Rend. sem. mat. fis., XLIII, (1973), Milano
[47] Mac Lane, S., Categories for the working Mathematician, (1971), Springer Berlin · Zbl 0232.18001
[48] Martin-Löf, P., Notes on constructive mathematics, (1970), Almqvist and Wiksell Stockholm · Zbl 0273.02021
[49] Martin-Löf, P., Lecture notes on the domain interpretation of type theory, ()
[50] Matthews, S., Metric domains for completeness, Ph.D. thesis, (1985), Univ. Warwick
[51] Milne, R.E.; Strachey, C., A theory of programming language semantics, (1976), Chapman & Hall London
[52] Milner, R., Fully abstract models of typed λ-calculi, Theoret. comput. sci., 4, 1, 1-22, (1977) · Zbl 0386.03006
[53] Milner, R., A calculus for communicating systems, Lecture notes in comput. sci., 92, (1980), Springer Berlin · Zbl 0452.68027
[54] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 3, 267-310, (1983) · Zbl 0512.68026
[55] Mycroft, A., Abstract interpretation and optimising transformations for applicative programs, Ph.D. thesis, (1981), Univ. Edinburgh
[56] Nielsen, F., Abstract interpretation using domain theory, Ph.D. thesis, (1984), Univ. Edinburgh
[57] Nivat, M., Infinite words, infinite trees, infinite computations, (), 3-52 · Zbl 0423.68012
[58] Oles, F.J., Type categories, functor categories and block structure, (), 543-574
[59] Plotkin, G.D., A powerdomain construction, SIAM J. comput., 5, 452-487, (1976) · Zbl 0355.68015
[60] Plotkin, G.D., LCF considered as a programming language, Theoret. comput. sci., 5, 3, 223-255, (1977) · Zbl 0369.68006
[61] Plotkin, G.D., Post-graduate lecture notes in advanced domain theory (incorporating the “pisa notes”), (1981), Dept. Comput. Sci., Univ. Edinburgh
[62] Plotkin, G.D., A powerdomain for countable non-determinism, (), 412-428 · Zbl 0511.68032
[63] Plotkin, G.D., A metalanguage for predomains, ()
[64] Plotkin, G.D., Lectures on predomains and partial functions, Notes for a course given at the center for the study of language and information, (1985), Stanford
[65] Plotkin, G.; Stirling, C., A framework for intuitionistic modal logics (extended abstract), (), 399-506
[66] Pnueli, A., The temporal logic of programs, Proc. 19th ann. symp. on the foundations of computer science, (1977), IEEE Computer Soc. Press Silver Spring, MD
[67] Poigné, A., On specifications, theories and models with higher types, Inform. and control, 68, (1986) · Zbl 0591.68019
[68] Poigné, A., Foundations are rich institutions, but institutions are poor foundations, Draft paper, (1987), Imperial College
[69] Pratt, V.R., Dynamic logic, (), 53-84 · Zbl 0433.68031
[70] Robinson, E., Logical aspects of denotational semantics, Summer conference on category theory and computer science, lecture notes in comput. sci., (1988), Springer Berlin · Zbl 0641.68024
[71] Schmidt, D.A., Denotational semantics, (1986), Allyn & Bacon Newton, MA
[72] Scott, D.S., Outline of a mathematical theory of computation, 4th ann. Princeton conference on information sciences and systems, 169-176, (1970)
[73] Scott, D.S., Data types as lattices, SIAM J. comput., 5, 522-587, (1976) · Zbl 0337.02018
[74] Scott, D.S., Lambda calculus: some models, some philosophy, (), 223-265
[75] Scott, D.S., Lectures on a mathematical theory of computation, Monograph PRG-19, (1981), Computing Laboratory, Oxford Univ.
[76] Scott, D.S., Domains for denotational semantics, () · Zbl 0495.68025
[77] Smyth, M.B., Effectively given domains, Theoret. comput. sci., 5, 3, 257-274, (1977) · Zbl 0429.03028
[78] Smyth, M.B., The largest Cartesian closed category of domains, Theoret. comput. sci., 27, 1,2, 109-119, (1983) · Zbl 0556.68017
[79] Smyth, M.B., Powerdomains and predicate transformers: a topological view, (), 662-675
[80] Smyth, M.B.; Plotkin, G.D., The category-theoretic solution of recursive domain equations, SIAM J. comput., 11, 761-783, (1982) · Zbl 0493.68022
[81] Soare, R.I., Recursively enumerable sets and degrees, Perspect. math. logic, (1987), Springer Berlin · Zbl 0667.03030
[82] Stirling, C., Modal logics for communicating systems, Theoret. comput. sci., 49, 2,3, 311-347, (1987) · Zbl 0624.68019
[83] Stone, M.H., The theory of representations for Boolean algebras, Trans. amer. math. soc., 37-111, (1936) · Zbl 0014.34002
[84] J.E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language theory, MIT Press Ser. Comput. Sci. (MIT Press, Cambridge, MA). · Zbl 0503.68059
[85] Vickers, S.J., Uscc, Draft paper, (1987), Imperial College London
[86] Vickers, S.J., Topology via logic, Cambridge tracts theoret. comput. sci., (1988), Cambridge Univ. Press Cambridge
[87] Winskel, G., Events in computation, Ph.D. thesis, (1980), Univ. Edinburgh
[88] Winskel, G., A complete proof system for SCCS with modal assertions, (), 392-410, Lecture Notes in Comput. Sci.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.