## How to prove a compiler correct (cross-post)

## Monotonicity Types: Towards A Type System for Eventual Consistency

A few weeks back, we published a draft of an article entitled *Monotonicity Types*. In it, we describe a type system which we hope can aid the design of distributed systems by tracking monotonicity with types.

## Final Algebra Semantics is Observational Equivalence

Recently, “final encodings” and “finally tagless style” have become popular techniques for defining embedded languages in functional languages. In a recent discussion in the Northeastern PRL lab, Michael Ballantyne, Ryan Culpepper and I asked “in what category are these actually final objects”? As it turns out our very own Mitch Wand wrote one of the first papers to make exactly this idea precise, so I read it available here and was pleasantly surprised to see that the definition of a final algebra there is essentially equivalent to the definition of observational equivalence.

In this post, I’ll go over some of the results of that paper and explain the connection to observational equivalence. In the process we’ll learn a bit about categorical logic, and I’ll reformulate some of the category theory in that paper to be a bit more modern in presentation, cleaning some things up in the process.

## PLT Redex FAQ

A short guide to Redex concepts, conventions, and common mistakes.

## Why am I going to ICFP 2017? (cross-post)

## Closure Conversion as CoYoneda

The continuation-passing style transform (cps) and closure conversion (cc) are two techniques widely employed by compilers for functional languages, and have been studied extensively in the compiler correctness literature. Interestingly, *typed* versions of each can be proven to be equivalence preserving using polymorphic types and parametric reasoning, as shown by my advisor Amal Ahmed and Matthias Blume (cps,cc).

In fact, there is something like a duality between the two proofs, cps uses a universal type, closure-conversion uses an existential type and the isomorphism proofs use analogous reasoning. It turns out that both are instances of general theorems in category theory: the polymorphic cps isomorphism can be proven using the Yoneda lemma, and the polymorphic closure-conversion isomorphism can be proven using a less well known theorem often called the *co*Yoneda lemma.

The connection between cps and the Yoneda embedding/lemma is detailed elsewhere in the literature and blogosphere (ncafe, Bartosz), so I’ll focus on closure conversion here. Also, I’ll try to go into some detail in showing how the “usual” version of Yoneda/coYoneda (using the category of sets) relates to the appropriate version for compilers.

I’ll assume some background knowledge on closure conversion and parametricity below. Fortunately, Matt Might has a nice blog post explaining untyped closure conversion.

## Gradual Typing Across the Spectrum, part II

Last week, Northeastern hosted a PI meeting for the Gradual Typing Across the Spectrum NSF grant. The meeting was made of 20+ researchers from four institutions, and 12 technical talks. Schedule:

http://prl.ccs.neu.edu/gtp/pi2017/pi2017.html

A common thread among the talks was the question: *how to convert a research idea into a tool for software developers?*

## Reviews and author responses: we should stop asking for 500-word responses

This year I reviewed many ICFP submissions, and got to be on the receiving end of equally many author responses (also sometimes called, somewhat combatively, rebuttals). I found that there was a large difference between the official written advice on author responses and what I, as a reviewer reading the responses, found effective. In particular, I now believe that limiting yourself to 500 words should strongly be avoided — we should even stop giving that advice.

## Trees, 1973

From the PRL archives:

I think that I shall never see a matrix lovely as a tree. —

Trees, by Guy L. Steele Jr., MIT, 1973