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
Great paper: The Calculated Typer
•
Aaron Stump
•
Season 7
•
Episode 6
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton. The authors take a very nice general look at the specification of a type checker, for a very simple expression language. They then manually derive the actual code for the type checker by effectively trying to prove that this as yet unknown code satisfies its spec. (This is what is meant by calculating the type checker.)