Past Meetup

Jay Sulzberger on Lambda Equivalence

This Meetup is past

74 people went

Location image of event venue

Details

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!

Meta Abstract

"On FizzBuzz, including an Introduction to the Dream of Homotopy Type Theory"

or

"On the Several Differences between Lisp and the Lambda Calculus"

or

"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."

References

When are two proofs the same?:

http://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs
http://math.stackexchange.com/questions/1242043/when-are-two-proofs-the-same

https://gowers.wordpress.com/2007/10/04/when-are-two-proofs-essentially-the-same/

https://homotopytypetheory.org/

https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/

https://en.wikipedia.org/wiki/Cryptomorphism

Gian-Carlo Rota's note on Alonzo Church:

https://www.princeton.edu/mudd/finding_aids/mathoral/pmcxrota.htm

Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay:
https://arxiv.org/abs/0903.0340

Lectures on the Curry-Howard Isomorphism, May 1998 not final version by M. H. B. Sorenson and P. Urzyczyn:
ftp://ftp.cs.cmu.edu/user/ftp/user/rwh/www/home/course/logic/www-old/handouts\ /curry-howard.pdf

Tom Stuart's delightful "Programming with Nothing": http://codon.com/programming-with-nothing

J. R. Hindley's 1997 book Basic Simple Type Theory:
https://mathtrielhighschool.files.wordpress.com/2011/08/number-theory.pdf

On FizzBuzz:

https://en.wikipedia.org/wiki/Fizz_buzzFizz

https://www.rosettacode.org/wiki/FizzBuzz

Bio

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.