<p>I continue the discussion of <a href='https://poplmark-reloaded.github.io/pdf/main.pdf'>POPLmark Reloaded</a> , discussing the solutions proposed to the benchmark problem.  The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.</p>

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.

<p>I continue the discussion of <a href="https://poplmark-reloaded.github.io/pdf/main.pdf" rel="noopener noreferrer">POPLmark Reloaded</a> , discussing the solutions proposed to the benchmark problem.&nbsp; The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.</p>

POPLmark Reloaded, Part 2

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share POPLmark Reloaded, Part 2

Sign up to save your podcasts

POPLmark Reloaded, Part 2

POPLmark Reloaded, Part 2

More shows like Iowa Type Theory Commute

Dwarkesh Podcast

Type Theory Forall