On the adequacy of per models

  • Roberto M. Amadio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


We consider a fixed point extension of the second order lambda calculus equipped with a call by value evaluation mechanism. We interpret the language in a partial cartesian closed category of “directed complete” partial equivalence relations (pers) over a domain theoretic model of a type-free, call-by-value, lambda calculus. Our main result is that the notions of “syntactic” and “semantic” convergence coincide.


Second order lambda-calculus Per models Denotational vs. Operational Semantics 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Amadio R. [1989] “Recursion over realizability structures”, Info.&Comp., 91, 1, (55–85), 1991. Also appeared as TR 1/89 Dipartimento di Informatica, Università di Pisa.Google Scholar
  2. [2]
    Amadio R. [1990] “Domains in a Realizability Framework”, in Proc. CAAP91, Brighton, SLNCS 493, Abramsky S., Maibaum T. (eds.), (241–263), full version appeared as Liens TR 19-90.Google Scholar
  3. [3]
    Amadio R. [1992] “On the adequacy of per models”, RR 1579 Inria-Lorraine, January 1992 (20 pages).Google Scholar
  4. [4]
    Amadio R., Cardelli L. [1990] “Subtyping Recursive Types”, in Proc. ACM-POPL91, Orlando. Full version appeared as DEC-SRC TR #62 and TR 133 Inria-Lorraine, in press on ACM-TOPLAS.Google Scholar
  5. [5]
    Baeten J, Boerboom B. [1979] “Ω can be anything it shouldn't be”, Indag. Math. 41, (111–120).Google Scholar
  6. [6]
    Cardelli L. [1989] “The Quest language and system”, internal note, DEC-SRC, Palo Alto.Google Scholar
  7. [7]
    Cardelli L., Longo G.[1990] “A semantic basis for Quest”, ACM-Lisp and F. P. 90, Nice.Google Scholar
  8. [8]
    Freyd P., Mulry P., Rosolini G., Scott D. [1990] “Extensional Pers”, 5th IEEE-LICS, Philadelphia.Google Scholar
  9. [9]
    Girard J.Y., Lafont Y., Taylor P. [1989] “Proofs and Types”, Cambridge University Press.Google Scholar
  10. [10]
    Hyland M. [1991] “First steps in synthetic domain theory”, in Proc. Category Theory 90, Como, Carboni&al. (eds.). Springer-Verlag.Google Scholar
  11. [11]
    Martin-Löf [1983] “The domain interpretation of type theory”, in Proc. Workshop on the Semantics of Programming Languages, Dybierd&al (eds.), Chalmers University, Göteborg.Google Scholar
  12. [12]
    Moggi E. [1988] “Partial morphisms in categories of effective objects”, Info.&Comp., 76, (250–277).Google Scholar
  13. [13]
    Plotkin G. [1985] “Denotational semantics with partial functions”, lecture notes, CSLI, Stanford 1985.Google Scholar
  14. [14]
    Rosolini G. [1986] “Continuity and effectiveness in Topoi”, PhD Thesis, Oxford University.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Roberto M. Amadio
    • 1
  1. 1.CRIN-CNRS & Inria-LorraineVandœuvre-lès-NancyFrance

Personalised recommendations