Polymorphic at last!

After a brief excursion into category theory, Tikhon will return to the lambda calculus and free it from the shackles of monomorphism.

Also, let's talk about some of the other activities we might be interested in pursuing in smaller groups. Those activities might include:

. Coding up interpreters on variations of the lambda calculus to build a small programming language

. Studying Coq and interactive theorem proving

. Studying a dependently-typed language like Agda or Idris

. Investigating homotopy type theory (I still have no idea what that is, but "homotopy" is a cool-sounding word)

. Jointly watching some of the Oregon Programming Languages Summer School lectures

. Or anything else you think we might be interested in

I'd like to get a headcount at the next meeting to see how many people might be interested in these activities. If you want to participate, try to figure out which days and times work best for you, and let me know if you know of any venues that might be able to accommodate a small group at those times (maybe with food and coffee), and whether you'd like to lead the activity in question.

I'm assuming we'll also keep going concurrently with the current lecture-style meeting format, as long as Tikhon or anyone else has something they want to talk about.