[Mads Buch] Proving Stuff in Haskell
Details
Talk by Mads Buch https://www.madsbuch.com/
(Virtual beers afterwards!)
In recent years organizations have started to realize the potential to use types in their engineering setups. In particular, we have seen a move from Javascript to Typescript. This unlocks productivity potentials in the form of fewer bugs and integrated type-driven editor support. But it also unlocks the ability to see one's program as the combination of logical language, the types, and proofs for the logics, the programs. This Curry-Howard correspondence is another way to view types and terms in programming. We will explore this perspective and hopefully enrich our understanding of the programs we write.
Though we will relate the principles to common languages, our main vehicle will be Haskell. In other words, we will be proving stuff in Haskell.
Bio: Mads Buch is a computer scientist from Aarhus University where he developed an interest for functional programming and type theory. He has since started a consultancy and explored the rice fields of Bali and the Corona lock-down in San Francisco.
THIS MEETUP WILL BE HELD ONLINE AT THE FOLLOWING URL:
https://meet.jit.si/mfk-april-2021