Dependent Types

  • February 10, 2014 · 7:00 PM
  • Mixrank

Our tour of the lambda calculi is approaching its high point, the dependently typed lambda calculus. After telling us how to use lambda calculus to make terms from terms and terms from types, Tikhon will show us how to make types from terms, thereby greatly simplifying some things while complicating others.

Also, it looks as if we have quora for exploring at least a couple of different topics:

. Dependent types and theorem proving through Coq and/or Idris

. Coding of lambda calculus interpreters

. And perhaps logic programming

Yet to be decided is just how to organize the subgroups on these topics, and when and where to meet. Tikhon has set up a new Google group for us to discuss these topics (and others) at https://groups.google.com/forum/#!forum/sf-ttpl, because many people find the meetup.com interface inconvenient for discussions.

Remember: *1111 opens the gate at Mixrank!

Join or login to comment.

  • Byron H.

    This cast some clarity on dependent types, which are a complex subject.

    February 13, 2014

  • Tikhon J.

    Also: please join the Google group: https://groups.google.com/forum/#!forum/sf-ttpl.

    February 13, 2014

  • Tikhon J.

    I finally put the slides for dependent types and System F (from last time) up on http://jelv.is. Yay.

    February 13, 2014

  • Sergei W.

    Sorry, I've been sick and couldn't attend. Hope to see the talk online in some form!

    February 11, 2014

  • Ian Z.

    So what is the front door protocol? Last time I got quite desperate and was about to give up and leave, but just at that point someone let me in.

    February 4, 2014

    • Adrian K.

      Type *1111 on the keypad at the door.

      February 4, 2014

    • Dave D.

      I ended up leaving last time...although to be perfectly honest, I might have gotten the date wrong. =(

      February 4, 2014

People in this
Meetup are also in:

Imagine having a community behind you

Get started Learn more
Bill

I started the group because there wasn't any other type of group like this. I've met some great folks in the group who have become close friends and have also met some amazing business owners.

Bill, started New York City Gay Craft Beer Lovers

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