Collection of slides, notes, and posters for public talks I've given.
A Case Study With Neural Networks
Dependently-typed Haskell is all about pushing the limits of how much power your types have to verify that your code is correct, direct you in writing code, enhance your productivity, and encode meaning in type signatures. In this session, we will explore its practical benefits by applying these principles to building verified neural networks. We look at neural networks with and without dependent types, show how to add dependently typed benefits incrementally, and clearly show the benefits that we can directly apply to many different applications. This session is geared less toward the theoretical idea of dependent types and more toward hitting the ground running with immediate benefits in existing code bases.
Developers will learn the basic concepts of dependent types, existential types, type-level proofs, and working with the “singletons” library, as well as high-level concepts in dependently typed development.
Super-charge the correctness of your code incrementally and find new ways to make the compiler work for you today!