When it comes to reasoning about programs, you may have heard of alpha and beta equivalence and possibly even eta equivalence, but you probably never heard of lambda equivalence and you won't find it with Google Search.
To learn about this exciting new technique please join us as the illustrious Jay Sulzberger presents Lambda Equivalence for the very first time!
"On FizzBuzz, including an Introduction to the Dream of Homotopy Type Theory"
"On the Several Differences between Lisp and the Lambda Calculus"
"The Paradigm Case of Curry-Howard [that is, for the Simply Typed Lambda Calculus] Helps Tell When Two Proofs of a Given Proposition are Really The Same."
When are two proofs the same?:
Gian-Carlo Rota's note on Alonzo Church:
Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay:
Lectures on the Curry-Howard Isomorphism, May 1998 not final version by M. H. B. Sorenson and P. Urzyczyn:
Tom Stuart's delightful "Programming with Nothing": http://codon.com/programming-with-nothing
J. R. Hindley's 1997 book Basic Simple Type Theory:
Jay Sulzberger has an honorary PhD in Mathematics from the Hogwarts School of Witchcraft and Wizardry (http://harrypotter.wikia.com/wiki/Hogwarts_School_of_Witchcraft_and_Wizardry) where he now serves as a board member. He worked at the the IBM Research Center for countless decades. He has been the resident Mathematician at Lisp NYC since 2002. His brilliance and wisdom are infinitely unenumerable. His favorite theorem is Bell's Theorem. He has proven on numerous occasions, using no more than three napkins, that Haskell is a lie.