Logical Semantics for the First Order ς-Calculus

  • Steffen van Bakel
  • Ugo de’Liguoro
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


We investigate logical semantics of the first order ς-calculus. An assignment system of predicates to first order typed terms of the OB1 calculus is introduced. We define retraction models for that calculus and an interpretation of terms, types and predicates into such models. The assignment system is then proved to be sound and complete w.r.t. retraction models.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  2. 2.
    Abadi, M., Plotkin, G.D.: A Per Model of Polymorphism and Recursive Types. In: Proc. of IEEE-LICS, pp. 3355–3365 (1990)Google Scholar
  3. 3.
    Abramsky, S.: Observation Equivalence and Testing Equivalence. Theoretical Computer Science 53, 225–241 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Abramsky, S.: Domain Theory in Logical Form. APAL 51, 1–77 (1991)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Amadio, R.: Recursion over Realizability Structures. Info. Comp. 91, 55–85 (1991); Theoretical Computer Science 102(1), 135–163 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    van Bakel, S.: Intersection Type Assignment Systems. Theoretical Computer Science 151(2), 385–435 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Barendregt, H.P., Coppo, M., Dezani, M.: A Filter Lambda Model and the Completeness of Type Assignment. JSL 48, 931–940 (1983)zbMATHCrossRefGoogle Scholar
  8. 8.
    Bruce, K.B., Mitchell, J.C.: PER models of subtyping, recursive types and higher-order polymorphism. In: Proc. of ACM-POPL 1992 (1992)Google Scholar
  9. 9.
    Cardone, F.: Relational semantics for recursive types and bounded quantification. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 164–178. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  10. 10.
    Coppo, M., Dezani, M., Venneri, B.: Functional characters of solvable terms. Grund. Der Math. 27, 45–58 (1981)zbMATHCrossRefGoogle Scholar
  11. 11.
    Dezani, M., Giovannetti, E., de’ Liguoro, U.: Intersection types, λ-models and Böhm trees. In: [19], pp. 45-97Google Scholar
  12. 12.
    de’Liguoro, U.: Characterizing convergent terms in object calculi via intersection types. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, p. 315. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    de’Liguoro, U.: Subtyping in logical form. In: ITRS 2002. ENTCS, vol. 70.1, Elsevier, Amsterdam (2002)Google Scholar
  14. 14.
    Kamin, S.: Inheritance in Smalltalk-80: a denotational definition. In: Proc. of POPL 1988, pp. 80–87 (1988)Google Scholar
  15. 15.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. of ACM 32(1), 137–161 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Krivine, J.L.: Lambda-calcul, types et modèles, Masson (1990)Google Scholar
  17. 17.
    Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
  18. 18.
    Scott, D.: Data types as lattices. SIAM J. Comput. 5(3), 522–587 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Takahashi, M., Okada, M., Dezani, M. (eds.): Theories of Types and Proofs. Mathematical Society of Japan, vol. 2 (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Steffen van Bakel
    • 1
  • Ugo de’Liguoro
    • 2
  1. 1.Department of ComputingImperial CollegeLondonUK
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Personalised recommendations