addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscontroller-playcrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramFill 1light-bulblinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonprintShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

Polymorphic at last!

  • Jan 27, 2014 · 7:00 PM
  • Mixrank

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.

Join or login to comment.

  • Tikhon J.

    I set up a google groups mailing list for the meetup. You can see it here:!forum/sf-ttpl

    January 28, 2014

  • Juan P.

    Missed the last meeting. FYI found via CACM:

    January 28, 2014

  • baltostar

    Could someone please let me in front door ?

    January 27, 2014

    • baltostar

      Yeah I must have left right before you went out there - I kept on calling Mixrank #04 and always got Google voice mail. Could we post the door policy for future meetups ?

      January 27, 2014

    • Adrian K.

      Very sorry we missed you! For future reference, the entry code on the keypad at the front door is *1111 (very high security).

      1 · January 28, 2014

  • Byron H.

    I'm also interested in learning about dependent types.
    Sorry to miss, but I'm so swamped.

    January 27, 2014

  • Kenny B.

    Something came up at work. Next time!

    January 27, 2014

  • A former member
    A former member

    I'm interested in learning more about dependent types.

    More generally, I'm interested in what insights from the type-theoretic world can be applied to imperative programming.

    January 22, 2014

  • Christopher B.

    For anyone interested, the Bay Area Categories and Types meetup is starting a new series on linear type theory (type theories based on linear logic) and its categorical interpretation, with applications to functional programming. A number of OPLSS luminaries and leading figures in the types community, including Bob Harper, Frank Pfenning, and Benjamin Pierce, have published in this area, as has BACAT co-organizer Valeria de Paiva. This group typically attracts a mix of Real Mathematicians and mere mortal software engineers like myself who enjoy a challenge. The organizers realy know their stuff. The new meeting series looks like it will be oriented pretty far toward the Real Mathematician end of the spectrum -- there was talk of collectively authoring a paper reflecting current state of the art in this area. I expect it will be fascinating and difficult.

    January 20, 2014

  • Christopher B.

    An intro to Agda is one of two talks scheduled for the Feb 6 meeting of Haskell Hackers at Hacker Dojo in Mountain View.

    January 16, 2014

  • Christopher B.

    For anyone interested, there is a Bay Area Categories and Types meeting Friday Jan 17 -- this is a social and planning meeting for next steps in that meetup.

    January 15, 2014

    • Jack F.

      I just got to your post the morning after the event. I've been busy w/ my new job and would not have been able to attend anyway. Can you give a synopsis of the typical meeting of this group and where they are going? I'm going to try to attend our 1/27 meetup and drag my new boss along.

      January 18, 2014

  • Sergei W.

    My interests:

    50% Coding an interpreter of lambda-calculus and/or other language
    25% certified programming with dependent types, Coq/Agda/Idris
    25% logic-based approaches (logic programming, temporal logic, declarative reactive programming)

    January 15, 2014

    • Sergei W.

      Actually I'd say, certified programming is 50% and coding interpreter is 25%.

      January 17, 2014

  • Christopher B.

    Responding to the survey request -- I'm particularly interested in Coq, Agda, Idris, homotypy type theory, Oregon PL videos, and type-level programming in functional languages.

    January 15, 2014

    • Adrian K.

      Chris, that sounds like an abuse of the term "particularly"­ -- you seem particularly interested in almost everything. (Me too.)

      1 · January 15, 2014

    • Christopher B.

      Guilty as charged. :) But I did omit coding of sample lambda calculi (not because I don't find that interesting, but it's not as high a priority for me).

      January 15, 2014

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