John Greiner's Research

In general, I'm interested in using theory, particularly programming language theory such as semantics and type theory, to design, analyze, and implement practical programming languages.


This page outlines, in chronological order, the projects I have worked on and gives references to my papers.

Scheme and Hygienic macro expansion

First I ported Scheme84 from being implemented in Franz Lisp to Common Lisp. Then I worked on improvements, primarily of the macro expansion of Scheme88 and ISWYM, which were unreleased modifications of Scheme84 and predecessors of Rice Scheme. This work was under the supervision of Matthias Felleisen (Rice University, 1988-89).

No published papers.

Using (co)induction and (co)inductive types in programming

This work reviews the theoretical aspects and explores the practical aspects of using induction and coinduction, rather than recursion, in programming. Coinduction admits data denoting infinite objects, such as the familiar stream data type. (Co)Induction is more restricted than general recursion (and similarly, (co)inductive types are more restricted than general ML-style datatypes), as all programs must terminate. But this work explores what can be programmed with (co)induction, and some idioms used in such programming. This was under the guidance of Bob Harper (CMU, 1991), and served as my Area Qualifier Major.

Published paper:

Weak polymorphism

I explored the implementation of SML/NJ's "weak types", which are used for typing side-effecting expressions such as "ref" cells, continuations, and exceptions. This was accomplished by reverse-engineering the implementation in SML/NJ and formalizing its key aspects. In particular, I showed that a simplification of SML/NJ's weak type system (especially similar to that in Version 0.66) is sound. This was under the guidances of Bob Harper (CMU, 1992-93).

Published papers:

Parallel algorithms for connected components

I looked at pragmatic aspects of several concurrent read concurrent write (CRCW) algorithms for finding the connected components of arbitrary graphs. This was the first published empirical comparison of such algorithms. This work was under the guidance of Guy Blelloch and with some help from Marco Zagha (CMU, 1993-94) and included my Area Qualifier Minor.

Published papers:

Complexity models based on programming languages

I explored the possibilities of adding cost measures to operational semantics to serve as the foundation for defining complexity in realistic programming languages, particularly functional languages. I am concentrating on the theoretical aspects of parallel implementations of call-by-value and call-by-speculation languages. This thesis work was under the guidance of Guy Blelloch (CMU, 1993-1997).

Some of the ideas of this work are as follows:

Published papers: