Applications of the Kleene–Kreisel Density Theorem to Theoretical Computer Science

  • Dag Normann

The Kleene–Kreisel density theorem is one of the tools used to investigate the denotational semantics of programs involving higher types.We give a brief introduction to the classic density theorem, then show how this may be generalized to set theoretical models for algorithms accepting real numbers as inputs, and finally survey some recent applications of this generalization.


Polish Space Density Theorem High Type Domain Theory Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramsky, S. and Jung, A., Domain Theory, in S. Abramsky, D.M. Gabbay and T.S.E. Maibaum (eds.), Handbook of Logic in Computer Science, vol. 3, Clarendon Press (1994)Google Scholar
  2. 2.
    Amadio, R. M. and Curien, P. -L. , Domains and Lambda-Calculi, Cambridge University Press (1998)Google Scholar
  3. 3.
    Bauer, A., Escardó, M.H. and Simpson, A., Comparing Functional Paradigms for Exact Real-number Computation, in Proceedings ICALP 2002, Springer LNCS 2380, 488-500 (2002)Google Scholar
  4. 4.
    Berger, U., Totale Objekte und Mengen in der Bereichtheorie (in German), Thesis, München (1990)Google Scholar
  5. 5.
    DeJaeger, F., Calculabilité sur les Réels, Thesis, Paris VII (2003)Google Scholar
  6. 6.
    DiGianantonio, P., A Functional Approach to Computability on Real Numbers, Thesis, Università di Pisa - Genova - Udine, (1993)Google Scholar
  7. 7.
    DiGianantonio, P., Real number computability and domain theory, Inform. and Comput.127,11-25 (1996)CrossRefMathSciNetGoogle Scholar
  8. 8.
    DiGianantonio, P., An abstract data type for real numbers, Theoret. Comput. Sci. 221,295-326 (1999)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Ershov, Yu. L., Maximal and everywhere defined functionals, Algebra and Logic 13, 210-225(1974)MATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gandy, R.O. and Hyland, J.M.E., Computable and recursively countable functions of higher type, Logic Colloquium ’76, 407-438, North-Holland (1977)Google Scholar
  11. 11.
    Hyland, J.M.E., Recursion on the Countable Functionals, Dissertation, Oxford (1975)Google Scholar
  12. 12.
    Kleene, S. C., Recursive functionals and quantifiers of finite types I, Trans. Amer. Math. Soc. 91, 1-52 (1959)MATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Kleene, S. C., Countable Functionals, in A. Heyting (ed.) Constructivity in Mathematics,81-100, North-Holland (1959)Google Scholar
  14. 14.
    Kreisel, G. , Interpretation of Analysis by Means of Functionals of Finite Type, in A. Heyting (ed.) Constructivity in Mathematics, North-Holland, 101-128 (1959)Google Scholar
  15. 15.
    Longley, J.R., On the ubiquity of certain total type structures, Electr. Notes Theor. Com-put. Sci. 73, 87-109 (2004) Google Scholar
  16. 16.
    Longo, G. and Moggi, E., The hereditary partial effective functionals and recursion the-ory in higher types, J. Symbolic Logic 49, 1319-1332 (1984)MATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Milner, R., Fully abstract models for typed λ-calculi, Theoret. Comput. Sci. 4, 1-22 (1977)MATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Moldestad, J., Computations in Higher Types, Springer Lecture Notes in Mathematics No. 574, Springer Verlag (1977)Google Scholar
  19. 19.
    Normann, D., The continuous functionals; computations, recursions and degrees, Annals of Mathematical Logic 21, 1-26 (1981)MATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Normann, D., Computing with functionals - computability theory or computer science?, Bull. Symbolic Logic 12(1), 43-59, (2006)MATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Normann, D., Computability over the partial continuous functionals, J. Symbolic Logic 65,1133-1142 (2000)MATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Normann, D., The Cook-Berger problem - A guide to the solution, Electr. Notes Theor. Comput. Sci. 35, (2000)Google Scholar
  23. 23.
    Normann, D., The Continuous Functionals of Finite Types over the Reals, in K. Keimel, G.Q. Zhang, Y. Liu and Y. Chen (eds.) Domains and Processes, Kluwer Academic Publishers, 103-124, (2001)Google Scholar
  24. 24.
    Normann, D., Hierarchies of total functionals over the reals, Theoret. Comput. Sci. 316, pp. 137-151 (2004)MATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Normann, D., Definability and reducibility in higher types over the reals, to appear in the proceedings og Logic Colloquium ’03Google Scholar
  26. 26.
    Normann, D., Comparing hierarchies of total functionals, Logical Methods in Computer Science 1(2), (2005)Google Scholar
  27. 27.
    Platek, R. A., Foundations of Recursion Theory, Thesis, Stanford University (1966)Google Scholar
  28. 28.
    Plotkin, G., LCF considered as a programming language, Theoret. Comput. Sci. 5, 223-255(1977)CrossRefMathSciNetGoogle Scholar
  29. 29.
    Plotkin, G., Full abstraction, totality and P CF , Math. Struct. in Comp. Science, 11, 1-20 (1999)CrossRefGoogle Scholar
  30. 30.
    Schröder, M., Admissible representations of limit spaces, in J. Blanck, V. Brattka, P. Hertling and K. Weihrauch (eds.), Computability and Complexity in Analysis, vol. 237, Informatik Berichte, 369-388, (2000)Google Scholar
  31. 31.
    Scott, D., A type-theoretical alternative to ISWIM, CUCH, OWHY, Unpublished notes, Oxford (1969). Printed with suplementary comments in Theoret. Comput. Sci. 121, 411-440 (1993) MATHGoogle Scholar
  32. 32.
    Simpson, A., Lazy functional Algorithms for Exact Real Functionals, Mathematical Foun-dations of Computer Science 1998, Springer LNCS 1450, 456-464, (1998)MathSciNetGoogle Scholar
  33. 33.
    Stoltenberg-Hansen, V., Lindström, I. and Griffor, E.R., Mathematical Theory of Do-mains, Cambridge Tracts in Theor. Comp. Sci. 22, Cambridge University Press (1994)Google Scholar
  34. 34.
    Tait, W.W., Continuity properties of partial recursive functionals of finite type, unpub-lished notes (1958)Google Scholar
  35. 35.
    Weihrauch, K., Computable Analysis, in Texts in Theoretical Computer Science, Springer Verlag, Berlin, (2000)Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2008

Authors and Affiliations

  • Dag Normann
    • 1
  1. 1.Department of MathematicsUniversity of OsloOsloNorway

Personalised recommendations