Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Abadi, M., Plotkin, G.D.: A Per Model of Polymorphism and Recursive Types. In: Proc. of IEEE-LICS, pp. 3355–3365 (1990)
Abramsky, S.: Observation Equivalence and Testing Equivalence. Theoretical Computer Science 53, 225–241 (1987)
Abramsky, S.: Domain Theory in Logical Form. APAL 51, 1–77 (1991)
Amadio, R.: Recursion over Realizability Structures. Info. Comp. 91, 55–85 (1991); Theoretical Computer Science 102(1), 135–163 (1992)
van Bakel, S.: Intersection Type Assignment Systems. Theoretical Computer Science 151(2), 385–435 (1995)
Barendregt, H.P., Coppo, M., Dezani, M.: A Filter Lambda Model and the Completeness of Type Assignment. JSL 48, 931–940 (1983)
Bruce, K.B., Mitchell, J.C.: PER models of subtyping, recursive types and higher-order polymorphism. In: Proc. of ACM-POPL 1992 (1992)
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)
Coppo, M., Dezani, M., Venneri, B.: Functional characters of solvable terms. Grund. Der Math. 27, 45–58 (1981)
Dezani, M., Giovannetti, E., de’ Liguoro, U.: Intersection types, λ-models and Böhm trees. In: [19], pp. 45-97
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)
de’Liguoro, U.: Subtyping in logical form. In: ITRS 2002. ENTCS, vol. 70.1, Elsevier, Amsterdam (2002)
Kamin, S.: Inheritance in Smalltalk-80: a denotational definition. In: Proc. of POPL 1988, pp. 80–87 (1988)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. of ACM 32(1), 137–161 (1985)
Krivine, J.L.: Lambda-calcul, types et modèles, Masson (1990)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)
Scott, D.: Data types as lattices. SIAM J. Comput. 5(3), 522–587 (1976)
Takahashi, M., Okada, M., Dezani, M. (eds.): Theories of Types and Proofs. Mathematical Society of Japan, vol. 2 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Bakel, S., de’Liguoro, U. (2003). Logical Semantics for the First Order ς-Calculus. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive