×

Principal type scheme and unification for intersection type discipline. (English) Zbl 0656.68022

The intersection type discipline for the \(\lambda\)-calculus (ITD) is an extension of the classical functionality theory of Curry. In the ITD a term satisfying a given property has a principal type scheme in an extended meaning, i.e., there is a type scheme deducible for it from which all and only the type schemes deducible for it are reachable, by means of suitable operations. The problem of finding the principal type scheme for a term, if it exists, is semidecidable. In the paper a procedure is shown, building the principal type scheme of a term through the construction of the most general unifier for intersection type schemes.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B40 Combinatory logic and lambda calculus

Software:

ML
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barendregt, H., The Lambda Calculus: its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007
[2] Barendregt, H.; Coppo, M.; Dezani, M., A filter λ-model and the completeness of type assignment, J. Symbolic Logic, 84, 931-940 (1983) · Zbl 0545.03004
[3] Berta, M., Schema di tipo principale per la disciplina dei tipi con intersezione, (Dissertazione di Laurea (1987), Dipartimento di Informatica: Dipartimento di Informatica Torino)
[4] Coppo, M.; Dezani, M., An extension of the basic functionality theory for the λ-calculus, Notre Dame J. Formal Logic, 21, 685-693 (1980) · Zbl 0423.03010
[5] Coppo, M.; Dezani, M.; Venneri, B., Principal type scheme and λ-calculus semantics, (Seldin, J. P.; Hindley, J. R., H.B. Curry. Essays on Combinatory Logic, λ-Calculus and Formalism (1980), Academic Press: Academic Press London), 535-560
[6] Curry, H. B.; Feys, R., Combinatory Logic, Vol. 1 (1958), North-Holland: North-Holland Amsterdam · Zbl 0175.27601
[7] Hindley, R., The principal type scheme as an object in combinatory logic, Trans. Amer. Math. Soc., 146, 29-60 (1969) · Zbl 0196.01501
[8] Hindley, R., The completeness theorem for typing λ-terms, Theoret. Comput. Sci., 22, 1-17 (1983) · Zbl 0512.03009
[9] Milner, R., A theory of type polymorphism in programming, J. Comput. System Sci., 17, 348-375 (1978) · Zbl 0388.68003
[10] Milner, R.; Damas, L., Principal type schemes for functional programs, Proc. 9th Symp. on Principles of Programming Languages, 207-212 (1982)
[11] Robinson, J. A., A machine oriented logic based on the resolution principle, J. ACM, 12, 23-41 (1965) · Zbl 0139.12303
[12] Ronchi Della Rocca, S., Characterization theorems for a filter lambda model, Inform. and Control, 54, 201-216 (1982) · Zbl 0513.03008
[13] Ronchi Della Rocca, S.; Venneri, B., Principal type scheme for an extended type theory, Theoret. Comput. Sci., 28, 151-169 (1984) · Zbl 0535.03007
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.