I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton. The authors take a very nice general look at the specification of a type checker, for a very simple expression language. They then manually derive the actual code for the type checker by effectively trying to prove that this as yet unknown code satisfies its spec. (This is what is meant by calculating the type checker.)

In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS). I sketch how CPS conversion (transforming a program with callcc into one in CPS that does not need callcc any more) corresponds to double-negation translation from classical to intuitionistic logic. The paper I am referencing is here.

In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming languages where formulas in logic are identified with types, and proofs with programs). This is the identification of double-negation translations in logic, which go back to a paper of Kolmogorov's in 1925, with conversion to continuation-passing style (CPS), a compilation technique. For this episode, we just discuss the idea of double-negation translation: classical theorems can be translated to intuitionistic ones, by adding some double negations. As an example, we talk through the intuitionistic proof of the double negation of the law of excluded middle: not not (p or not p).