×

Intersection types and computational rules. (English) Zbl 1264.03045

de Queiroz, Ruy (ed.) et al., Proceedings of the 10th workshop on logic, language, information and computation (WoLLIC’2003), Ouro Preto, Minas Gerais, Brazil, July 29 – August 1, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 84, 45-59 (2003).
Summary: The invariance of the meaning of a \(\lambda \)-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements for a \(\lambda \)-model. Being the intersection type systems a general framework for the study of semantic domains for the lambda calculus, the present paper provides a characterisation of “meaning invariance” in terms of characterisation results for intersection type systems enabling typing invariance of terms w.r.t. various notions of reduction/expansion, like \(\beta , \eta \) and a number of relevant restrictions of theirs.
For the entire collection see [Zbl 1109.03307].

MSC:

03B40 Combinatory logic and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abadi, M.; Cardelli, L.; Curien, P.L.; Levy, J.-J., Explicit substitutions, J. of functional progr, 1, 4, 375-416, (1991) · Zbl 0941.68542
[2] Abramsky, S., Domain theory in logical form, Ann. pure appl. logic, 51, 1-2, 1-77, (1991) · Zbl 0737.03006
[3] Abramsky, S.; Luke Ong, C.-H., Full abstraction in the lazy lambda calculus, Inform. and comput, 105, 2, 159-267, (1993) · Zbl 0779.03003
[4] Alessi, F.; Dezani-Ciancaglini, M., Filter models and easy terms, (), 17-37 · Zbl 1042.03014
[5] Alessi, F.; Lusin, S., Simple easy terms, ITRS’02 volume 70 of ENTCS, (2002), Elsevier · Zbl 1270.03028
[6] 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
[7] Coppo, M.; Dezani-Ciancaglini, M., An extension of the basic functionality theory for the λ-calculus, Notre dame J. formal logic, 21, 4, 685-693, (1980) · Zbl 0423.03010
[8] Coppo, M.; Dezani-Ciancaglini, M.; Venneri, B., Functional characters of solvable terms, Z. math. logik grundlag. math, 27, 1, 45-58, (1981) · Zbl 0479.03006
[9] Coppo, M.; Dezani-Ciancaglini, M.; Zacchi, B., Type theories, normal forms, and D_{∞}-lambda-models, Inform. and comput, 72, 2, 85-116, (1987) · Zbl 0645.03011
[10] Coppo, M.; Honsell, F.; Dezani-Ciancaglini, M.; Longo, G., Extended type structures and filter lambda models, (), 241-262 · Zbl 0558.03007
[11] Curry, H.B.; Feys, R., combinatory logic, volume I of studies in logic and the foundations of mathematics, (1958), North-Holland
[12] Dezani-Ciancaglini, M.; Ghilezan, S., Two behavioural lambda models, (), 127-147 · Zbl 1023.03022
[13] Dezani-Ciancaglini, M.; Honsell, F.; Motohama, Y., Compositional characterization of λ-terms using intersection types, (), 304-313 · Zbl 0996.03501
[14] Engidi, L.; Honsell, F.; Ronchi, S.; Rocca, Della, Operational, denotational and logical descriptions: a case study, Fund. inform, 16, 2, 149-169, (1992) · Zbl 0762.68042
[15] Engeler, E., Algebras and combinators, Algebra universalis, 13, 3, 389-392, (1981) · Zbl 0482.08005
[16] Gierz, G.K.; Hoffmann, K.H.; Keimel, K.; Mislove, J.D.; Scott, D.S., A compendium of continuous lattices, (1980), Springer-Verlag · Zbl 0452.06001
[17] Honsell, F.; Lenisa, M., Some results on the full abstraction problem for restricted lambda calculi, (), 84-104 · Zbl 0925.03095
[18] Honsell, F.; Lenisa, M., Semantical analysis of perpetual strategies in λ-calculus, Theoret. comput. sci, 212, 1-2, 183-209, (1999) · Zbl 0913.68132
[19] Honsell, F.; Ronchi, S.; Rocca, Della, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, J. comput. system sci, 45, 1, 49-75, (1992) · Zbl 0763.03012
[20] Kamareddine, F.; Rios, A.; Wells, J.B., Calculi of generalized beta-reduction and explicit substitution: type free and simply typed versions, J. of functional and logic progr, 5, 1-44, (1998)
[21] D. Park. The Y-combinator in Scott’s λ-calculus models (revised version). Theory of Computation Report 13, Department of Computer Science, University of Warick, 1976.
[22] Plotkin, G.D., Call-by-name, call-by-value and the λ-calculus, Theoret. comput. sci, 1, 2, 125-159, (1975) · Zbl 0325.68006
[23] Plotkin, G.D., Set-theoretical and other elementary models of the λ-calculus, Theoret. comput. sci, 121, 1-2, 351-409, (1993) · Zbl 0790.03014
[24] Scott, D.S., Continuous lattices, (), 97-136
[25] Scott, D.S., Open problem, (), 369
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.