February 10, 2014 · 7:00 PM
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!