A Taste of Type Theory • Bartosz Milewski • YOW! 2019

This presentation was recorded at YOW! 2019. #GOTOcon #YOW https://yowcon.com Bartosz Milewski - Founder of Reliable Software ABSTRACT We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory. I can't possibly talk about all of this, but I'll try to give you a little taste. [...] TIMECODES 0:00 Introduction 2:19 Outline 5:09 Equalities 9:51 Natural Numbers 16:29 Dependent Types 23:38 Induction on Nats 27:23 Curry Howard 30:28 Identity Type 35:36 refl 42:48 Elimination 52:51 Zeno's Paradox https://twitter.com/GOTOcon https://www.linkedin.com/company/goto- https://www.facebook.com/GOTOConferences #TypeTheory #Haskell #Programming #DataTypes #Algebra #BartoszMilewski #YOWcon Looking for a unique learning experience? Attend the next GOTO conference near you! Get your ticket at https://gotopia.tech Sign up for updates and specials at https://gotopia.tech/newsletter SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily. https://www.youtube.com/user/GotoConferences/?sub_confirmation=1