A lambda-calculus for dynamic binding. (English) Zbl 0895.68015

Summary: Dynamic binding is a runtime lookup operation which extracts values corresponding to some “names” from some “environments” (finite, unordered associations of names and values). Many situations related with flexible software assembly involve dynamic binding: first-class modules, mobile code, object-oriented message passing. This paper proposes \(\lambda N\), a compact extension of the \(\lambda\)-calculus to model dynamic binding, where variables are labelled by names, and where arguments are passed to functions along named channels. The resulting formalism preserves familiar properties of the \(\lambda\)-calculus, has a Curry-style-type inference system, and has a formal notion of compatibility for reasoning about extensible environments. It can encode records and record extensions, as well as first-class contexts with context-filling operations, and therefore provides a basic framework for expressing a wide range of name-based coordination mechanisms. An experimental functional language based on \(\lambda N\) illustrates the exploitation of dynamic binding in programming language design.


68N15 Theory of programming languages
Full Text: DOI


[1] Abramsky, S.; Ong, C.-H.L., Full abstraction in the lazy lambda calculus, Inform. comput., 105, 159-267, (1993) · Zbl 0779.03003
[2] ()
[3] M. Banville, Sonia: an adaptation of linda for coordination of activities in organizations, in: [9], pp. 57-74.
[4] Barendregt, H., The lambda-calculus, its syntax and semantics, studies in logic and the foundations of mathematics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[5] Breazu-Tannen, V.; Coquand, T.; Gunter, C.A.; Scedrov, A., Inheritance as implicit coercion, Inform. comput., 93, 172-221, (1991), also in: [14], pp. 197-245. · Zbl 0799.68129
[6] Bruce, K.; Longo, G., A modest model of records, inheritance, and bounded quantification, Inform. comput., 87, 196-240, (1990), also in: [14], pp. 151-195. · Zbl 0711.68072
[7] Cardelli, L., A semantics of multiple inheritance, Inform. comput., 76, 138-164, (1988) · Zbl 0651.68017
[8] Cardelli, L.; Mitchell, J., Operations on records, mathematical structures in computer science, (), 3-48, also in: [14], pp. 295-350.
[9] ()
[10] Dami, L., Type inference and subtyping for higher-order generative communication, (), 98-138
[11] Harper, R.; Pierce, B., A record calculus based on symmetric concatenation, (), 131-142
[12] Florijn, G.; Besamusca, T.; Greefhorst, D., Ariadne and hopla: flexible coordination of collaborative processes, (), 197-214
[13] Garrigue, J.; Aït-Kaci, H., The typed polymorphic label-selective lambda calculus, (), 35-47
[14] ()
[15] Hashimoto, M.; Ohori, A., A typed context calculus, (), available at · Zbl 0989.68017
[16] Hudak, P., The Haskell report and Haskell tutorial, ACM SIGPLAN notices, 27, 5, (1992)
[17] Jagannathan, S., Dynamic modules in higher-order languages, (), 74-87
[18] Lamping, J., A unified system of parameterization for programming languages, (), 316-326
[19] Lee, S.-D.; Friedman, D.P., Enriching the lambda calculus with contexts: towards a theory of incremental program construction, (), 239-250, (6) · Zbl 1344.68051
[20] Milner, R.; Tofte, M.; Harper, R., The definition of standard ML, (1991), MIT Press New York
[21] Queinnec, C.; de Roure, D., Sharing code through first-class environments, (), 251-261, (6)
[22] Radestock, M.; Eisenbach, S., Semantics of a higher-order coordination language, (), 339-356
[23] Rémy, D., Typechecking records and variants in a natural extension of ML, (), 242-249, also in: [14], pp. 67-96.
[24] Rémy, D., Typing record concatenation for free, (), 166-176, also in: [14], pp. 351-372. · Zbl 0837.68058
[25] Talcott, C., A theory of binding structures and applications to rewriting, Theoret. comput. sci., 112, 99-143, (1993) · Zbl 0783.68089
[26] Takahashi, M., Parallel reductions in λ-calculus, Inform. comput., 118, 1, 120-127, (1995) · Zbl 0827.68060
[27] Wand, M., Type inference for record concatenation and multiple inheritance, Inform. comput., 93, 1, 1-15, (1991) · Zbl 0732.68026
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.