×

Polymorphic type inference and containment. (English) Zbl 0656.68023

Type expressions may be used to describe the functional behaviour of untyped lambda terms. A semantics for quantified types over arbitrary models of untyped lambda calculus is presented. Completeness theorems for inference models without empty types, simple inference models, quotient- set semantics of types as well as for models that may have empty types are proven. Containment relation on types is used to get some insight into the set of quantified types associated with a term. To that end containments that hold in all semantic models are investigated using a pure type assignment system based on containment.
Reviewer: L.Brim

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B40 Combinatory logic and lambda calculus
68Q65 Abstract data types; algebraic specification

Software:

ML
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Barendregt, H.P., ()
[2] Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda model and the completeness of type assignment, J. symbolic logic, 48/4, 931-940, (1983) · Zbl 0545.03004
[3] Bruce, K.B.; Meyer, A.R.; Mitchell, J.C., The semantics of second-order lambda calculus, Inform. and control, (1987), in press
[4] Coppo, M.; Zacchi, M., Type inference and logical relations, (), 218-226
[5] Curry, H.B.; Feys, R., ()
[6] Damas, L.; Milner, R., Principal type schemes for functional programs, (), 207-212
[7] Dezani-Ciancaglini, M.; Margaria, I., F-semantics for intersection type discipline, (), 279-300, Sophia-Antipolis (France) · Zbl 0552.68006
[8] Donahue, J., On the semantics of data type, SIAM J. comput., 8, 546-560, (1979) · Zbl 0418.68010
[9] Fortune, S.; Leivant, D.; O’Donnell, M., The expressiveness of simple and second order type structure, J. assoc. comput. March., 30, 1, 151-185, (1983) · Zbl 0519.68046
[10] Friedman, H., Equality between functionals, (), 22-37
[11] Girard, J.Y., Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur, ()
[12] Gordon, M.J.; Milner, R.; Wadsworth, C.P., Edinburgh LCF, () · Zbl 0421.68039
[13] Henkin, L., Completeness in the theory of types, J. symbolic logic, 15, 2, 81-91, (1950) · Zbl 0039.00801
[14] Hindley, R., The principal type-scheme of an object in combinatory logic, Trans. amer. math. soc., 146, 29-60, (1969) · Zbl 0196.01501
[15] Hindley, R., The completeness theorem for typing lambda terms, Theoret. comput. sci., 22, 1-17, (1983) · Zbl 0512.03009
[16] Hindley, R., Curry’s type rules are complete with respect to the F-semantics too, Theoret. comput. sci., 22, 127-133, (1983) · Zbl 0512.03010
[17] Hyland, J.M.E., A syntactic characterization of the equality in some models of the lambda calculus, J. London math. soc., 2, 12, 361-370, (1976) · Zbl 0329.02010
[18] Kreisel, G., Interpretation of analysis by means of constructive functionals of finite types, (), 101-128
[19] Leivant, D., Polymorphic type inference, (), 88-98
[20] MacQueen, D.; Sethi, R., A semantic model of types for applicative languages, (), 243-252
[21] MacQueen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, Inform. and control, 71, 1/2, 95-130, (1986) · Zbl 0636.68016
[22] McCracken, N., The typechecking of programs with implicit type structure, (), 301-316
[23] Meyer, A.R., What is a model of the lambda calculus?, Inform. and control, 52, 1, 87-122, (1982) · Zbl 0507.03002
[24] Meyer, A.R.; Mitchell, J.C.; Moggi, E.; Statman, R., Empty types in polymorphic lambda calculus, (), 253-262
[25] Milner, R., A theory of type polymorphism in programming, J. comput. system sci., 17, 348-375, (1978) · Zbl 0388.68003
[26] Milner, R., The standard ML core language, Polymorphism, 2, 2, 28, (1985), an earlier version appeared in “Proc. 1984 ACM Symp. on Lisp and Funcional Programming.”
[27] Mitchell, J.C., Coercion and type inference (summary), (), 175-185
[28] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential types, (), 37-51
[29] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (), 308-319
[30] Myhill, J.R.; Shepherdson, J.C., Effective operations on partial recursive functions, Z. math. logik grundlag. math., 1, (1955) · Zbl 0068.24706
[31] Paterson, M.S.; Wegman, M.N., Linear unification, J. comput. system sci., 16, 158-167, (1978) · Zbl 0371.68013
[32] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[33] Robinson, J.A., A machine oriented logic based on the resolution principle, J. assoc. comput. Mach., 12, 1, 23-41, (1965) · Zbl 0139.12303
[34] Scott, D., Data types as lattices, SIAM J. comput., 5, 3, 522-587, (1976) · Zbl 0337.02018
[35] Statman, R., Equality between functionals, revisited, (), 331-338
[36] Troelstra, A.S., Mathematical investigation of intuitionistic arithmetic and analysis, () · Zbl 0227.02015
[37] Wadsworth, C., The relation between computational and denotational properties for Scott’s D∞ models, SIAM J. comput., 5, 3, 488-521, (1976) · Zbl 0346.02013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.