Domains in a realizability framework

  • Roberto M. Amadio
CAAP Colloquium On Trees In Algebra And Programming
Part of the Lecture Notes in Computer Science book series (LNCS, volume 493)


We aim to relate and develop various approaches to a theory of domains in a realizability framework.

In the first part we develop the theory in an arbitrary partial cartesian closed category and, as a particular instance, in the category of partial equivalence relations (per) over an arbitrary partial combinatory algebra (pca). In this way one obtains the category of separated pers that may be regarded as a universe of partially ordered sets and monotone maps with strong closure properties.

Pursuing the analogy with domain theory one tries to build a category of directed complete partial orders and continuous maps. We consider two main approaches: one based on Kleene's pca of numbers and partial recursive functions and the other based on Scott's D λ-model.

Contents: 0. Introduction, 1. Dominance and Intrinsic Preorder, 2. Separated Partial Equivalence Relations (Σper), 3. N-completeness, 4. Σ-connection and Extensionality, 5. D-completeness and Uniformity, 6. Conclusion.


Full Subcategory Terminal Object Realizability Framework Admissible Family Partial Recursive Function 
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.


  1. Abadi M., Plotkin G. [1990] "A per model of polymorphism and recursive types", 5th IEEE-LICS, Philadelphia.Google Scholar
  2. Amadio R. [1989] "Recursion over realizability structures", TR 1/89 Dipartimento di Informatica, Università di Pisa, (to appear on Info.&Comp.).Google Scholar
  3. Amadio R., Cardelli L. [1990] "Subtyping Recursive Types", DEC-SRC TR #62, ext. abs. to appear in Proc. ACM-POPL91.Google Scholar
  4. Bruce K., Longo G. [1990] "A modest model of records, inheritance and bounded quantification", Info&Comp., 87, 1–2, (196–240), Preliminary version in Proc. of IEEE-LICS 88.Google Scholar
  5. Carboni A., Freyd P., Scedrov A. [1987] "A categorical approach to realizability and polymorphic types" 3rd ACM Symp. on Math. Found of Language semantics, New Orleans.Google Scholar
  6. Cardelli L., Longo G. [1990] "A semantic basis for Quest", in Proc LISP&FP, Nice.Google Scholar
  7. Coppo M. [1985] "A completeness theorem for recursively defined types", in Proc. 12th ICALP, Nafplion, Greece 1985, SLNCS 194.Google Scholar
  8. Curien P-L., Obtulowicz A. [1988] "Partiality, Cartesian Closedness and Toposes", Information & Computation, 80, (50–95).Google Scholar
  9. Droste M., Göbel R. [1990] "Universal domains in the theory of denotational semantics of programming languages", IEEE-LICS 90, Philadelphia.Google Scholar
  10. Freyd P., Mulry P., Rosolini G., Scott D. [1990] "Extensional Pers", 5th IEEE-LICS, Philadelphia.Google Scholar
  11. Gunter C., Jung A. [1990] "Coherence and Consistency in Domains", J.P.Apl.Alg., 63, (49–66).Google Scholar
  12. Hyland M. [1982] "The effective Topos," in The Brouwer Symposium, (Troelstra, Van Dalen eds.), North-Holland.Google Scholar
  13. Hyland M. [1988] "A small complete category", APAL, 40, 2, (135–165).Google Scholar
  14. Longo G., Moggi E. [1984] "Cartesian closed categories of enumerations for effective type-structures", in Symp. on Semantics of Data Types, Kahn&al. (eds.), SLNCS 173.Google Scholar
  15. Longo G., Moggi E. [1988] "Constructive Natural Deduction and its Modest Interpretation", CMU Report CS-88-131, Lecture delivered at the workshop "The semantics of natural and programming languages" Stanford, March 1987.Google Scholar
  16. Mac Lane S. [1971] "Categories for the working mathematician", Springer-Verlag, New York.Google Scholar
  17. McCarthy D. [1984] "Realizability and Recursive mathematics" Ph. D. Thesis, Merton College, Oxford.Google Scholar
  18. Moggi E. [1988] "Partial morphisms in categories of effective objects", Info.&Comp., 76, (250–277).Google Scholar
  19. Mulry P. [1981] "Generalized Banach-Mazur functionals in the topos of recursive sets", J. Pure Apl. Algebra, 26, 1, (71–83).Google Scholar
  20. Myhill J., Shepherdson J. [1955] "Effective operations on partial recursive functions", Zeit. für Math. Logik und Grund. der Math., 1, (310–317).Google Scholar
  21. Paulin-Mohring C. [1989] "Extraction de programmes dans le calcul des contructions", thèse, Paris VII.Google Scholar
  22. Phoa W. [1990] "Effective domains and intrinsic structure", 5th IEEE-LICS, Philadelphia.Google Scholar
  23. Plotkin G. [1980/4] "Domains", lecture notes, C.S. Dept., Edinburgh.Google Scholar
  24. Robinson E., Rosolini P. [1988] "Categories of partial maps", Info&Co., 79, (95–130).Google Scholar
  25. Rosolini G. [1986] "Continuity and effectiveness in Topoi" PhD Thesis, Oxford University.Google Scholar
  26. Scott D. [1976] "Data types as lattices," SIAM Journal of Computing, 5 (pp. 522–587).Google Scholar
  27. Smyth M. [1977] "Effectively Given Domains", Theoret. Comput. Sci. 5, (255–272).Google Scholar
  28. Smyth M., Plotkin G. [1982] "The category-theoretic solution of recursive domain equations" SIAM Journal of Computing 11, (pp.761–783).Google Scholar
  29. Soare R. [1987] "Recursively enumerable sets and degrees", Springer-Verlag.Google Scholar
  30. Streicher T. [1990] "Independence results for impredicative calculi of dependent types", preprint.Google Scholar
  31. Troelstra A., van Dalen D. [1988] "Constructivism in Mathematics", 2 vols., North-Holland.Google Scholar
  32. Wand M. [1979] "Fixed-point Constructions in Order-enriched Categories", Theoret. Comp. Sci. (13–30).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Roberto M. Amadio
    • 1
  1. 1.Labo. Informatique, Ecole Normale SupérieureParis

Personalised recommendations