A Friendly Introduction to the Lambda Calculus

LISP has its syntactic roots in a formal system called the lambda calculus. After a brief discussion of formal systems and logic in general, I will dive in to the lambda calculus and make enough constructions to convince you that it really is capable of expressing anything that is "computable". Time permitting, I will talk about the simply typed lambda calculus and the Curry-Howard-Lambek correspondence, which asserts that programs and mathematical proofs are "the same thing".

Dr. Dustin Mulcahey holds a PhD in Mathematics with a specialization in Homotopy Theory.