Double-negation translations and CPS conversion, part 1

Iowa Type Theory Commute by Aaron Stump

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 progr...View more