A Taste of Type Theory
YOW! Lambda Jam 2019
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.
Bartosz used to be a physicist (he has a Ph.D. in Quantum Physics) but he fell in love with programming and joined Microsoft as the development lead of the Content Index team -- the search engine before the Internet. Whenever you do a file search on Windows, you're running his code.
After Microsoft, Bartosz started his own company, Reliable Software, where he designed and helped implement the first peer-to-peer version control system, Code Co-op, which is still in commercial use.
He became an expert in C++ and published the book C++ In Action. He is best known for his blog, in which he discusses topics in concurrency, parallelism, language design, functional programming, and many other areas. He attended one C++ Standard Committee meeting on concurrency and decided that C++ was too far behind Haskell or even C# in this area. He's a frequent speaker at professional conferences about applications of category theory and type theory in programming.
He has been the architect of the FP Complete School of Haskell.
He published the book "Category Theory for Programmers."