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
DCS compared to termination checkers for type theories
•
Aaron Stump
•
Season 4
•
Episode 18
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.