zbMATH — the first resource for mathematics

Typing and computational properties of lambda expressions. (English) Zbl 0613.68020
This paper integrates and generalizes known techniques and results (in particular, by the works of Girard and Coppo, Dezani & Veneri) relating typing to convergence properties (such as normalizability) in the lambda calculus. It does so by considering types as semantical properties of $$\lambda$$-expressions in second-order models over $$\lambda$$-expressions. Working in the semantic discipline permits a richer notion of type and, therefore, more general results.
Reviewer: J.-J.Ch.Meyer

MSC:
 68Q65 Abstract data types; algebraic specification 68Q60 Specification and verification (program logics, model checking, etc.) 03B40 Combinatory logic and lambda calculus
Automath
Full Text:
References:
 [1] Andrews, P.B., Resolution in type theory, J. symbolic logic, 36, 414-432, (1971) · Zbl 0231.02038 [2] Barendregt, H., The lambda calculus, (1981), North-Holland Amsterdam · Zbl 0467.03010 [3] Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda-model and the completeness of type-assignment, J. symbolic logic, 48, 931-940, (1983) · Zbl 0545.03004 [4] Bruce, K.B.; Meyer, A.R., The semantics of second-order polymorphic lambda calculus, (), 131-144 [5] Coppo, M.; Dezani-Ciancaglini, M., An extension of basic functionality theory for λ-calculus, Notre-dame J. formal logic, 21, 685-693, (1980) · Zbl 0423.03010 [6] Coppo, M.; Dezani-Ciancaglini, M.; Veneri, B., Functional character of solvable terms, Z. math. logik grundlag. math., 27, 45-58, (1981) · Zbl 0479.03006 [7] Curry, H.B.; Feys, R., Combinatory logic, (1958), North-Holland Amsterdam · Zbl 0175.27601 [8] Church, A., A formulation of the simple theory of types, J. symbolic logic, 5, 56-68, (1940) · JFM 66.1192.06 [9] Coppo, M., An extended polymorphic type system for applicative languages, (), 194-204 [10] de Bruijn, N.G., The mathematical language AUTOMATH, its usage and some of its extensions, (), 29-61 · Zbl 0208.20101 [11] () [12] Fortune, S.; Leivant, D.; O’Donnell, M., The expressiveness of simple and second order type structures, J. ACM, 30, 151-185, (1983) · Zbl 0519.68046 [13] Friedman, H., Some applications of Kleene’s method for intuitionistic systems, (), 113-170 [14] Girard, J.-Y., Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types, (), 63-92 [15] Girard, J.-Y., Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur, (), Paris [16] Henkin, L., Completeness in the theory of types, J. symbolic logic, 15, 81-91, (1950) · Zbl 0039.00801 [17] Howard, W.A., The formulae-as-types notion of construction, (), 479-490 [18] Leivant, D., The complexity of parameter passing in polymorphic procedures, (), 38-45 [19] Leivant, D., Polymorphic type inference, (), 88-98 [20] Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, (), 460-469 [21] Martin-Löf, P., Hauptsatz for the theory of species, (), 217-234 [22] Morris, J., Lambda calculus models of programming languages, () [23] MacQueen, D.B.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, (), 165-174 [24] MacQueen, D.B.; Sethi, R., A semantic model of types for applicative languages, (), 243-252 [25] Pottinger, G., A type assignment to the strongly normalizable terms, (), 561-578 [26] Prawitz, D., Completeness and hauptsatz for second order logic, Theoria, 33, 246-258, (1967) · Zbl 0175.26702 [27] Prawitz, D., Hauptsatz for higher order logic, J. symbolic logic, 33, 452-457, (1968) · Zbl 0164.31002 [28] Prawitz, D., Ideas and results in proof theory, (), 235-308 [29] Reynolds, J.C., Towards a theory of type structures, (), 408-425 [30] Sanchis, L.E., Functionals defined by recursion, Notre-dame J. formal logic, 8, 161-174, (1967) · Zbl 0183.01403 [31] () [32] Stenlund, S., Combinators, λ-terms and proof theory, (1972), Reidel Dordrecht · Zbl 0248.02032 [33] Tait, W.W., A non-constructive proof of Gentzen’s hauptsatz for second order predicate logic, Bull. amer. math. soc., 72, 980-983, (1966) · Zbl 0199.00801 [34] Tait, W.W., Intensional interpretation of functionals of finite type, J. symbolic logic, 32, 198-212, (1967) · Zbl 0174.01202 [35] Tait, W.W., A realizability interpretation of the theory of species, (), 240-251 [36] Takahashi, Moto-O, A proof of cut-elimination theorem in simple type theory, J. math. soc. Japan, 19, 399-410, (1967) · Zbl 0206.27503 [37] Wadsworth, C.P., The relation between computational and denotational properties of Scott’s D∞-model of the lambda-calculus, SIAM J. comput., 5, 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.