Story behind the name

Why is the club named dependently-typed?

In the summer of 2021, I (Elton) was fortunate enough to be interning on the PyTorch Dev Infra team at Facebook. It was an eye-opening experience and I enjoyed my time there. Around mid-July, I scheduled some 1-on-1 time with Edward Yang who works on the PyTorch Composability team. Prior to Facebook, he worked on GHC (in particular the Backpack module system) and had the amazing opportunity of working with Sir Simon Peyton Jones. Chatting with him inspired me to learn how GHC works.

While browsing through the GHC wiki, I stumbled upon this paper by Richard Eisenberg titled "Dependent Types in Haskell: Theory and Practice". In case you are not familiar, dependent types are types which depend on values. You can, for example, define a type that depends on the length of a list (which is variable). This is very heavily used in proof assistants and formal verification languages like Coq and F*.

In the paper, Eisenberg acknowledges how the PLClub at Penn helped him throughout his PhD. After reading this, I thought to myself: "What if I start a PLClub at Georgia Tech?".

In honor of the paper, I decided to name the club dependently-typed :)