V. Bragilevsky - The Glasgow Haskell Compiler as an exercise in the type theory
Details
This meetup is hosted by @IndeedEng
Annotation:
One may think of type theory as a purely theoretical tool for studying lambda calculus. Can you imagine someone using the Turing machine to build a practical compiler? Well, this is exactly the case with the Haskell programming language. Every piece of the code in Haskell is translated by the Glasgow Haskell Compiler (GHC) into the typed lambda calculus and is then checked, optimized, and translated down further to the machine code. So, it is real and quite challenging.
In this talk, Vitaly Bragilevsky, author of “Haskell in Depth,” will introduce both type theory and GHC and show how they work together to compile programs in Haskell. We'll cover the process of compilation of Haskell programs and discuss which and how type theory elements are used. We'll also see how functional programming makes it easier to reason about such complex software as compilers and ensures their correctness.
Attendees will learn basics of the type theory, see how GHC utilizes it, and be prepared to read advanced papers on extending Haskell type system. Knowledge of type theory is not required to attend this talk. Knowledge of Haskell at the beginner's level is useful but is not required either, although functional programming background is essential.
About presenter
Vitaly Bragilevsky is a university lecturer in Computer Science, author of "Haskell in Depth" (https://www.manning.com/books/haskell-in-depth), Haskell language committee member (Haskell 2020), invited lecturer on LambdaConf etc.
Agenda
6.00 PM - 6.30 PM: Check In & Networking
6.30 PM - 8.00 PM: The Glasgow Haskell Compiler as an exercise in the type theory (speaker: Vitaly Bragilevsky)
8.00 PM - 8.30 PM Networking with fellow FP enthusiasts over some beer & food
Canceled
V. Bragilevsky - The Glasgow Haskell Compiler as an exercise in the type theory