Introduction to Dependent Types with Idris: Encoding Program Proofs in Types


Introduction to Dependent Types with Idris: Encoding Program Proofs in Types 1st ed. Edition
by Boro Sitnikovski(Author)
Publisher Finelybook 出版社: Apress; 1st ed. edition (March 18, 2023)
Language 语言: English
pages 页数: 175 pages
ISBN-10 书号: 1484292588
ISBN-13 书号: 9781484292587


Book Description
Dependent types are a concept that allows developers to write proof-carrying code. Idris is a programming language that supports dependent types. This book will teach you the mathematical foundations of Idris as well as how to use it to write software and mathematically prove properties.
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 types
Gain insight into functional programming
Write mathematical proofs with Idris

Who this book is for
Programmers, mathematicians, academics, and anyone else interested learning dependent types and lambda calculus.

打赏
未经允许不得转载:finelybook » Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

相关推荐

  • 暂无文章

觉得文章有用就打赏一下

您的打赏,我们将继续给力更多优质内容

支付宝扫一扫打赏

微信扫一扫打赏