addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupsimageimagesinstagramlinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1outlookpersonStartprice-ribbonImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruseryahoo

Whatever Comes after the Untyped Lambda Calculus

  • Dec 5, 2013 · 7:00 PM
  • Mixrank

Tikhon gave us the short and sweet introduction to the untyped lambda calculus. He's up for giving another talk next time. On the meetup page, go to More > Polls > What topic for our next meeting and vote on what you'd like to hear!

Join or login to comment.

  • Sergei W.

    I made a short write-up about lambda-calculus. Still trying to understand why we cannot implement the sum and product types without introducing them by hand. My comments during the meetup (about implementing the sum and product types) turned out to be incorrect!
    https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx3aW5pdHpraXxneDoyZTQyZGFjNjY5ODNiMWVj

    December 8, 2013

    • Sergei W.

      My remaining questions: 1. How can we establish that the product type cannot be implemented in simply typed lambda-calculus without introducing new types by hand? I'd like to see a proof by any rigorous method (Curry-Howard isomorphism, category theory, intuitionistic logic). 2. Is there some theoretical explanation for the fact that the sum type can be implemented but product type cannot?

      December 8, 2013

    • Sergei W.

      I aksed this question on Mathoverflow and got an interesting answer. Neither the sum nor the product types are correctly implementable in simply typed lambda-calculus. This can be proved rather easily using the CH isomorphism. http://mathoverflow.n...­

      December 9, 2013

  • Tikhon J.

    I put my slides up on http://jelv.is/talks. I'll also put up pdf versions once I figure out how to get org-mode to output to beamer :).

    December 7, 2013

  • Juan P.

    Thanks for the lecture and discussion, everyone! I'm looking forward to the future meetings. The basic mechanics of this stuff is straight forward. But it's the implications that interest me. Nice to get an appreciation for combinators. I'm studying everything I can find at the moment...

    December 6, 2013

  • A former member
    A former member

    Finally I have started understanding this stuff! Thank you Tikhon and all other experts!

    December 6, 2013

  • Byron H.

    Once again, I seem to have timed pout. I regret missing.

    December 5, 2013

  • A former member
    A former member

    My wife got sick so I'll be staying home to look after her. Looking forward to the next meet up.

    December 5, 2013

  • Sergei W.

    Discovered an interesting type theory course http://pauillac.inria.fr/~remy/mpri/ that is being taught right now at Jussieu (Université Paris 7) by Didier Rémy (one of the creators of OCaml). Lecture notes are being posted and revised.

    December 5, 2013

  • A former member
    A former member

    This conflicts with the SF Clojure meetup by the way.

    http://www.meetup.com/The-Bay-Area-Clojure-User-Group/events/133420002/

    I would ask that this group try to avoid overlap with FP language meetup groups in future.

    December 2, 2013

    • Adrian K.

      Darn it, you're right. We need a more complicated scheduling algorithm than just "every other Thursday".

      December 2, 2013

  • Adrian K.

    The poll is running 5 - 3 for the simply typed lambda calculus, which seems like a logical next step from the untyped lambda calculus. Tikhon, have you got something ready for us?

    December 2, 2013

    • Tikhon J.

      Okay, the simply typed lambda calculus sounds good.

      December 2, 2013

17 went

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy