Connecting...

W1siziisimnvbxbpbgvkx3rozw1lx2fzc2v0cy9zawduawz5lxrly2hub2xvz3kvanbnl2jhbm5lci1kzwzhdwx0lmpwzyjdxq

Haskell and Type Theory: Better Together by Vitaly Bragilevsky

W1siziisijiwmtkvmdivmjevmdkvmzkvmzcvntc4l3blegvscy1wag90by0xmdy4ntizlmpwzwcixsxbinailcj0ahvtyiisijkwmhg5mdbcdtawm2uixv0

Looking for a talk where you can learn about both Haskell and Type Theory? 

At F(by) Conference, Vitaly Bragilevsky showed us how theory can be fruitful and exciting and that Haskell can be seen from many points of view.

 

Haskell and Type Theory: Better Together

Haskell can be seen from many points of view: you can build web services with it or study category theory. My favourite one is Haskel as a practical application of a type theory, which is a lovely piece of theoretical computer science by itself. Why not see how they work together? 
 
Type theory is used in GHC to compile Haskell code. I'll first present lambda calculus and several type systems over it and then continue on with the demonstration how high-level code in Haskell is translated into the Core, intermediate language inside GHC, which is, in fact, a modest extension of Girard's System F. The talk is going to be split in half: 50% of type theory and 50% of Haskell and GHC internals. 
 
I don't expect any prior knowledge of type theory, basic acquaintance with Haskell will be useful to understand what is going on in the second part of the talk. The main idea of the talk is to justify the fact that theory can be quite fruitful and exciting.
 
 
This talk was given by Vitaly Bragilevsky at F(by) Conference 2018.