Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Podcasting since 2019 • 190 episodes
Iowa Type Theory Commute
Latest Episodes
A Fireball of Alpha
I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church. One reason to do that, besides just a love of being ornery, is to be able to state and prove theor...
•
Season 7
•
Episode 12
•
20:09
Solving Quadratic Word Equations
A system of word equations is called quadratic if no variable occurs more than twice in it. There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode. My source is Ch...
•
Season 7
•
Episode 11
•
22:45
A little bit about word equations
The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem. Word equations relate expressions consisting of concatenations of variables and constant symbols. An example is a X ...
•
Season 7
•
Episode 10
•
17:14