&lgr;-V-CS: an extended &lgr;-calculus for scheme

ABSTRACT

The &lgr;-v-CS-calculus is a conservative extension of the &lgr;-value-calculus for reasoning about programs in Scheme-like languages. The basis of the extended calculus is a symbolic rewriting semantics for imperative programs. We show with numerous examples how to state and prove equational properties of Scheme-programs in the calculus. The examples suggest that the algebraic manipulation of imperative-functional programs is as feasible and as fruitful as that of functional ones.

REFERENCES

• 1: BARENDREGT, H.P. The Lambda Calculus: its Syntax and Semantics. rev. ed. Studies in Logic and the Foundations of Mathematics 103. North- Holland, Amsterdam, 1984.
• 2: Matthias Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, 1987
• 3: M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 4: M Felleisen , D P Friedman, A reduction semantics for imperative higher-order languages, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.206-223, March 1987, Eindhoven, The Netherlands
• 5: FELLEISEN, M., D.P. FRIEDMAN, B. DUBA, AND J. MERRILL. Beyond continuations. Technical Report No 216, Indiana University Computer Science Department, 1987.
• 6: FRIEDMAN, D. Applications of continuations. Technical Report No. 237, Indiana Univeristy Computer Science Department, 1988.
• 7: Ralph E. Griswold , Madge T. Griswold, ICON Programmng Language, Prentice Hall Professional Technical Reference, 1983
• 8: Christopher T. Haynes, Logic continuations, Journal of Logic Programming, v.4 n.2, p.157-176, June 1, 19876 [doi>10.1016/0743-1066(87)90016-1]
• 9: Christopher T Haynes , Daniel P Friedman , Mitchell Wand, Obtaining coroutines with continuations, Computer Languages, v.11 n.3-4, p.143-153, 1986 [doi>10.1016/0096-0551(86)90007-X]
• 10: P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
• 11: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 12: MASON, I.A. Equivalences of first-order Lisp programs. In Proc. Symposium on Logic in Computer Science, 1986, 105-117.
• 13: Ian Alistair Mason, The semantics of destructive lisp (side-effects), 1986
• 14: MASON, I.A. AND C. TALCOTT. Programming, transforming, and proving with function abstractions and memories. Unpublished manuscript. 1988.
• 15: PLOTKIN, G.D. Call-by-name, call-by-vMue, and the A-calculus. Theor. Comput. $ci. 1, 1975, 125-159.
• 16: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 17: Guy Lewis Steele, Jr. , Gerald Jay Sussman, The dream of a lifetime: A lazy variable extent mechanism, Proceedings of the 1980 ACM conference on LISP and functional programming, p.163-172, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802802]
• 18: Guy L Steele , Gerald J Sussman, The Art of the Interpreter or, The Modularity Complex (Parts Zero, One, and Two), Massachusetts Institute of Technology, Cambridge, MA, 1978
• 19: STEELE, G.L., JR. AND G.J. SUSSMAN. The revised report on Scheme, a dialect of Lisp. Memo 452, MIT AI-Lab, 1978.
• 20: Gerald J. Sussman , Guy L. Steele, Jr., An Interpreter for Extended Lambda Calculus, Massachusetts Institute of Technology, Cambridge, MA, 1975
• 21: Carolyn L. Talcott, The essence of rum: a theory of the intensional and extensional aspects of lisp-type computation (program transformation, closure, continuation structure, comparison-relation), 1985

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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: SCHEME

General Terms:
Algorithms, Design, Languages