Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
POPLmark Reloaded, Part 2
•
Aaron Stump
•
Season 6
•
Episode 3
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.