A functional theory of local names

ABSTRACT

&lgr;v is an extension of the &lgr;-calculus with a binding construct for local names. The extension has properties analogous to classical &lgr;-calculus and preserves all observational equivalences of &lgr;. It is useful as a basis for modeling wide-spectrum languages that build on a functional core.

REFERENCES

• 1: H. P. Barendregt. The Lambda Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.
• 2: Erik Crank , Matthias Felleisen, Parameter-passing and the lambda calculus, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99616]
• 3: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 4: P. Hudak and D. Rabin. Mutable abstract datatypes - or - how to have your state and munge it too. Research Report YALEU/DCS/RR-914, Yale University, Department of Computer Science, July 1992.
• 5: J. Launchbury. Lazy imperative programming. In SIPL '93 A CM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, pages 46-56, June 1993. Yale University Research Report YALEU/DCS/RR-96S.
• 6: I. Mason , C. Talcott, A sound and complete axiomatization of operational equivalence of programs with memory, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.284-293, June 1989, Pacific Grove, California, United States
• 7: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 8: R. Milner. Functions as processes. Rapport de Recherche 1154, INRIA Sophia-Antipolis, February 1990.
• 9: Robin Milner, Elements of interaction: Turing award lecture, Communications of the ACM, v.36 n.1, p.78-89, Jan. 1993 [doi>10.1145/151233.151240]
• 10: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 11: M. Odersky. A syntactic theory of local names. Research Report YALEU/DCS/RR-965, Department of Computer Science, Yale University, May 1993.
• 12: M. Odersky and D. Rabin. The unexpurgated callby-name, assignment, and the lambda-calculus. Research Report YALEU/DCS/RR-930, Department of Computer Science, Yale University, May 1993.
• 13: Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158521]
• 14: Frank Joseph Oles, A category-theoretic approach to the semantics of programming languages, 1982
• 15: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 16: A. Pitts and I. Stark. On the observable properties of higher order functions that dynamically create local names. In SIPL '93 A CM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, pages 31-45, June 1993. Yale University Research Report YALEU/DCS/RR-968.
• 17: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.
• 18: J.C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.
• 19: Jon G. Riecke, Delimiting the scope of effects, Proceedings of the conference on Functional programming languages and computer architecture, p.146-155, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165200]
• 20: Vipin Swarup , Uday S. Reddy , Evan Ireland, Assignments for applicative languages, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.192-214, June 1991, Cambridge, Massachusetts, United States
• 21: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 22: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 23: Stephen Weeks , Matthias Felleisen, On the orthogonality of assignments and procedures in Algol, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-70, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158523]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory, Verification