In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s.  See this short note for Turing's original proof and some historical comment...

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods.  We will look at proofs in more detail in the coming episodes.  Feel free to join the...

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC).  But surprisingly, the type is non-uniform.  If we abbreviate (A -> A) -> A -> A as Nat...

It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC).  Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simpl...

I review the typing rules and some basic examples for STLC.  I also remind listeners of the Curry-Howard isomorphism for STLC.