On this page:
Texts on writing
Advice on memo 1 (ps1)
A proposal memo

Writing

communicating is more than half the game

Texts on writing

American editors use Strunk and White’s little book of rules to check the elements of style. Read it, read it again, and again. Late editions do not improve over early editions.

If you need a verbose description that addresses technical issues too, look for "Bugs in Writing."

Advice on memo 1 (ps1)

I will use the following dimensions to evaluate your descriptive memos:

A proposal memo

Below is a sample memo based on Matthias Felleisen’s experience with a paper by Plotkin which he encountered as a PhD student. He says it took him four months to understand the basics of the paper, and he then spent nearly ten years working out solutions to the implied problems that the paper poses.

Project Proposal

Call-by-name, Call-by-value, and the Lambda Calculus

Matthias Felleisen

Gordon Plotkin’s paper [1] studies the relationship between programming languages and Church’s lambda calculus. It specifically addresses the scientific debate of how the call-by-value parameter-passing mechanism in most programming languages relates to the beta rule of the calculus. Concretely, the paper presents two variants of Landin’s abstract SECD machine for evaluating lambda terms—one for evaluating according to call-by-name and one for call-by-value—and a variant of the lambda calculus for each of them. It then proves one set of theorems for each machine-calculus pairing: a Church-Rosser theorem, a Curry-Feys Standardization theorem, a theorem relating the standard reduction relation and the respective SECD, and a soundness theorem for the equational calculation system with respect to the observational equivalence relation generated by the SECD evaluator. The paper concludes with a section that relates the two calculation systems to each other via Fisher’s continuation-passing style transformation.

At this point, we fail to understand three aspects of these results. First, it remains unclear how the calculations in the by-name and by-value calculus differ for sample programs. Second, we are wondering how the equational calculation system relate to the standard reduction relation. Third, we wish to study Plotkin’s proof that the evaluation function based on the standard reduction function is the same as the one defined by Landin’s SECD abstract machine.

For the first two questions, we intend to build a call-by-name and a call-by-value calculus, respectively, with Redex. Then we will create a series of increasingly complex sample programs and study their reduction graphs, i.e., the graphs generated by the general reduction relation of the calculus. We expect that we can develop a strategy for identifying the standard reduction path(s) in these graphs. Finally, for the third question, we intend to break up Plotkin’s proof into smaller pieces, focusing on one abstract register from the SECD machine at a time. By transforming the machine one step at a time, the proof should become self-explanatory. We will initially focus on the proof for the call-by-value system; it should become obvious how to port this method to the call-by-name system.

1. Gordon Plotkin. Call-by-name, Call-by-value, and the Lambda Calculus. TCS 1974.

2. Michael Fisher. Lambda-Calculus Schema. Proceedings of ACM Conference on Proving Assertions, 1972.

Compare this memo with the proposed structure on the Project page.