Greg Sullivan's Papers

• Gregory T. Sullivan.
  Operationally-Based Models of Higher-Order Imperative Programming Languages
  Ph.D. Thesis, August 1997.

  We present a typed metalanguage with support for higher-order functions, a global store, and input-output. An operational, small-step semantics is given for the metalanguage, with the operations on the global store and for I/O restricted to continuation passing style. We develop, based solely on the operational semantics, a theory of term equivalence in the metalanguage, notably an Extensionality Theorem (also known as a context lemma). By considering equivalence classes of operationally equivalent metalanguage terms, we construct a term model which we then use as the target for denotational semantics of imperative programming languages. As an in-depth application of our methods, we prove correct a number of source-to-source transformations used in a compiler for Scheme.

  Also available: In DVI format,

• Gregory T. Sullivan and Mitchell Wand
  Incremental Lambda Lifting: An Exercise in Almost-Denotational Semantics
  Extended Abstract. Submitted for publication.

  We prove the correctness of incremental lambda-lifting, an optimization that attempts to reduce the closure allocation overhead of higher-order programs by changing the scope of nested procedures. This optimization is invalid in the standard denotational semantics of Scheme, because it changes the storage behavior of the program. Our method consists of giving Scheme a denotational semantics in an operationally-based term model in which interaction is the basic observable. Lambda lifting is then shown to preserve meaning in the model.

  Also available as a DVI file.

• Mitchell Wand and Gregory T. Sullivan.
  Denotational Semantics Using an Operationally-Based Term Model
  In Proceedings 23rd ACM Symposium on Programming Languages, 1997.

  We introduce a method for proving the correctness of transformations of programs in languages like Scheme and ML. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing that the transformation is meaning-preserving. This allows us to consider correctness for programs that interact with their environment without terminating, and also for transformations that change the internal store behavior of the program. We illustrate the technique on one of the Meyer-Sieber examples, and we use it to prove the correctness of assignment elimination for Scheme. The latter is an important but subtle step for Scheme compilers; we believe ours is the first proof of its correctness.

• Mitchell Wand and Gregory T. Sullivan.
  A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs
  Technical Report NU-CCS-95-19, Northeastern University College of Computer Science, October 1995.

  In a series of papers in the early 80's we proposed a paradigm for semantics-based compiler correctness. In this paradigm, the source and target languages are given denotational semantics in the same lambda-theory, so correctness proofs can be carried out within this theory. In many cases, the proofs have a highly structured form. We show how a simple proof strategy, based on an algorithm for alpha-matching, can be used to build a tool that can automate all the routine cases of these proofs.

• Gregory T. Sullivan and Karl Lieberherr.
  An Object-Oriented Design Methodology
  Technical Report NU-CCS-95-01, Northeastern University College of Computer Science, September 1993.

  This paper presents a methodology for software analysis and design and an associated graph-based representation. The methodology addresses the specification of both static and dynamic aspects of an application. The representation includes object-oriented data modeling features. The specifications are modular, reusable, and adaptive -- that is repercussions from underlying model modifications are limited. There is a straightforward process for generating code to implement the specifications in an object-oriented target language.