Reasoning with continuations II: full abstraction for models of control

ABSTRACT

A fully abstract model of a programming language assigns the same meaning to two terms if and only if they have the same operational behavior. Such models are well-known for functional languages but little is known about extended functional languages with sophisticated control structures. We show that a direct model with error values and the conventional continuation model are adequate for functional languages augmented with first- and higher-order control facilities, respectively. Furthermore, both models become fully abstract on adding a control delimiter and a parallel conditional to the programming languages.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers , John H. Williams, Program transformation in the presence of errors, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.210-217, December 1989, San Francisco, California, United States [doi>10.1145/96709.96730]
• 2: H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984. Revised edition.
• 3: V. Breazu-Tannen , C. A. Gunter , A. Scedrov, Computing with coercions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.44-60, June 27-29, 1990, Nice, France [doi>10.1145/91556.91590]
• 4: Olivier Danvy , Andrzej Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.151-160, June 27-29, 1990, Nice, France [doi>10.1145/91556.91622]
• 5: R. K. Dybvig , R. Hieb, Engines from continuations, Computer Languages, v.14 n.2, p.109-123, Aug. 1989 [doi>10.1016/0096-0551(89)90018-0]
• 6: Matthias Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, 1987
• 7: Matthias Felleisen, &lgr;-V-CS: an extended &lgr;-calculus for scheme, Proceedings of the 1988 ACM conference on LISP and functional programming, p.72-85, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62686]
• 8: 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]
• 9: M. Felleisen, On the expressive power of programming languages, Proceedings of the third European symposium on programming on ESOP '90, p.134-151, May 1990, Copenhagen, Denmark
• 10: M. Felleisen and R.S. Cartwright. Extended direct semantics. Technical Report 105, Rice University, January 1990.
• 11: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• 12: D.P. Friedman, C.T. Haynes, and E. Kohlbecker. Programming with continuations. In P. Pepper, editor, Program Transformations and Programming Environments, pages 263-274. Springer-Verlag, Heidelberg, 1985.
• 13: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 14: Christopher T. Haynes , Daniel P. Friedman, Embedding continuations in procedural objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.4, p.582-598, Oct. 1987 [doi>10.1145/29873.30392]
• 15: 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]
• 16: R. Hieb , R. Kent Dybvig, Continuations and concurrency, Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.128-136, March 14-16, 1990, Seattle, Washington, United States
• 17: John McCarthy, LISP 1.5 Programmer's Manual, The MIT Press, 1962
• 18: Albert Meyer , Jon G. Riecke, Continuations may be unreasonable, Proceedings of the 1988 ACM conference on LISP and functional programming, p.63-71, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62685]
• 19: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 20: G.D. Plotkin. Call-by-name, call-by-value, and the A-calcuhs. Theor. Comput. Sci., 1:125-159, 1975.
• 21: G.D. Plotkin. LCF considered as a programming l~nguage. Theor. Comput. $ci., 5:223- 255, 1977.
• 22: J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
• 23: Dorai Staram , Matthias Felleisen, Control delimiters and their hierarchies, Lisp and Symbolic Computation, v.3 n.1, p.67-99, Jan. 1990 [doi>10.1007/BF01806126]
• 24: Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
• 25: C. Strachey and C.P. Wadsworth. Continua.tions: A m~them~tical semantics for handling full jumps. Technical Report PRG-11, Oxford University Computing Laboratory, Programming Research Group, 1974.
• 26: Gerald J. Sussman , Guy L. Steele, Jr., An Interpreter for Extended Lambda Calculus, Massachusetts Institute of Technology, Cambridge, MA, 1975
• 27: 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
• 28: C. Talcott, Rum. An intensional theory of function and control abstractions, Lecture notes in computer science on Foundations of logic and functional programming, p.3-44, June 1988, Trento, Italy

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: LISP
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

General Terms:
Algorithms, Languages, Theory