GL—a denotational testbed with continuations and partial continuations as first-class objects

ABSTRACT

In this paper we describe GL, a language designed to support interactive experimentation with denotational semantics of programming languages, and the novel features of its interpreter. GL is an expressional language that might best be described as an implementation of lambda calculus augmented with several useful basic data types including 1-values.A unique aspect of the GL environment is that it presents a visible, user-accessible implementation of the continuation semantics of GL. The user is expected to understand a denotational definition of GL, and to interact with the system in terms of that definition. In particular, if a computation is temporarily halted the expression continuation extant at that point can be interactively captured and later applied to other values and stores. The implementation of this feature is via a pair of routines called setjmpup and longjmpup that provide what might be called a partial continuation facility. A partial continuation is a function over stores or store/value pairs that represents execution of a partially executed program from its current state to some later state possibly before its half state. The semantics of partial continuations is interesting, and an extension of GL is presented that contains continuations and partial continuations as first-class objects.The GL environment is fairly complete; it has an experimental polymorphic type inference mechanism that supports self-application and report likely sources of user error in a robust manner, and it has a flexible breakpoint and trace facility that permits program execution to be observed and controlled at a variety of levels of granularity. Moreover, it has been used successfully to teach a graduate course in Theory of Programming Languages.

REFERENCES

• 1: 1. Scott, D., "Data Types as Lattices," SIAM Journal of Computing 5(1976).
• 2: John C. Reynolds, G/EDANKEN—a simple typeless language based on the principle of completeness and the reference concept, Communications of the ACM, v.13 n.5, p.308-319, May 1970 [doi>10.1145/362349.362364]
• 3: 3. Sussman, Gerald Jay and Guy Lewis Steele, Jr., "Scheme: an interpreter for an extended lambda calculus," MIT Artificial Intellegence Memo 349 (December 1975).
• 4: Daniel P. Friedman , Christopher T. Haynes, Constraining control, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-254, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318654]
• 5: 5. Felleisen, Matthias, Daniel P. Friedman, Bruce Duba, and John Murrow, "Beyond Continuations," Tech Report #216, Indiana University Computer Science Department (February 1987).
• 6: 6. Joloboff, Vania. personal communication. December 1986.

INDEX TERMS

Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Experimentation, Languages, Theory