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).

Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it.

See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.

I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderful reference for this is this paper by Palsberg.