This post started off as an introduction to a post about the simply typed lambda calculus. It got a bit out of control – but reading it over, I think that it’s valuable background. So I’ve made it into its own post. ST type theory is an interesting idea, but it’s mostly interesting as a … Continue reading The Constructivist Roots of Type Theory