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