Iowa Type Theory Commute

POPLmark Reloaded, Part 1

Aaron Stump Season 6 Episode 2

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Language theory.