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

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

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

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

In this episode, I talk about what we should consider to be a measure function.  Such functions can be used to show termination of some process or program, by assigning a measure to each program, and showing that as the program computes, t...