Introduction to Dependent Types with Idris Encoding Program Proofs in Types

The first part of the book serves as an introduction to the language's underlying theories. It starts by reviewing formal systems and mathematical logical systems as foundational building blocks, then gradually builds up to dependent types. Next, you'll learn type theory for dependent types. Following this, you'll explore the Idris programming language and conclude by exploring the depths of formal systems and type checkers by implementing them.
Introduction to Dependent Types with Idris will walk you through simple examples through more advanced techniques, stepping up the difficulty as you gain more knowledge. Every chapter includes a set of exercises based on what it covered to further cement your learning. No specialized knowledge of mathematics is expected beyond the basics, so it is perfect for novices.
What You Will Learn Understand Lambda calculus and dependent typesGain insight into functional programmingWrite mathematical proofs with Idris
Who This Book Is For
Programmers, mathematicians, academics, and anyone else interested learning dependent types and lambda calculus.