Past Meetup

Bodil Stokke on "Basic Polymorphic Type Checking" by Luca Cardelli

This Meetup is past

108 people went

uSwitch

The Cooperage, 5 Copper Row, London, SE1 2LH · London

How to find us

Use Copper Row pedonal path, enter the little square with the mermaid fountain and search the stairs with the ZPG sign.

Location image of event venue

Details

Bodil Stokke (https://bodil.lol and https://twitter.com/bodil) presents the paper "Basic Polymorphic Type Checking" by Luca Cardelli. The paper is available here: http://lucacardelli.name/Papers/BasicTypechecking.pdf

Abstract

Cardelli's 1987 paper "Basic Polymorphic Type Checking" was, according to the author, the first attempt to explain the Hindley-Milner-Damas type system in a way that would be accessible to people who weren't either Hindley, Milner or Damas. It served as my first gentle introduction to the mysteries of type checking, back when I was obsessed with the conceit that the world needed another Lisp with a type system and I was going to have to build it (it would be called BODOL, because obviously).

It was my first significant journey into the mysteries of type checking, to a large extent because it delivers what it promises on the tin: it's an explanation of a method for type checking and inference with parametric polymorphism that's accessible to the average programmer, as opposed to the average logician, and so I'd like to share that journey by walking through and implementing the described type checker with you, but maybe in a language more accessible to modern programmers than the Modula-2 of Cardelli's implementation.

The Speaker

Born into an aristocratic Russian-German family, Bodil (https://bodil.lol https://twitter.com/bodil) traveled widely around the Soviet Union as a child. Largely self-educated, she developed an interest in computer science during her teenage years. According to her later claims, in 1989 she embarked on a series of world travels, visiting Europe, the Americas, and India. She alleged that during this period she encountered a group of mathematical adepts, the “Haskell Language and Library Committee,” who sent her to Glasgow, Scotland, where they trained her to develop her powers of category theory. Both contemporary critics and later biographers have argued that some or all of these foreign visits were fictitious, and that she spent this period writing JavaScript.

Bodil was a controversial figure during her lifetime, championed by supporters as an enlightened guru and derided as a fraudulent charlatan by critics. Her doctrines influenced the spread of Homotopy Type Theory in the West as well as the development of Western computer science currents like dependent types, blockchains and isomorphic JavaScript.

The meetup

PapersWeLove (http://paperswelove.org) London proudly brings to you the best papers every month! Please join us to read and discuss the most amazing ideas in computer science. We meet at ZPG (https://www.uswitch.com/about-us/contact-us/) offices near Tower Bridge (https://goo.gl/maps/qJXZek4fMNU2) with the following schedule:

• 6.30pm: networking, pizza and drinks.
• 7:00pm: presentation starts