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

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.

依賴型是一個概念，允許開發人員編寫具有證明功能的程式碼。Idris 是一種支援依賴型的程式語言。本書將教導您 Idris 的數學基礎，以及如何使用它來編寫軟體並數學上證明屬性。

本書的第一部分作為語言基礎理論的介紹。它從回顧形式系統和數學邏輯系統作為基礎建設模塊開始，然後逐漸發展到依賴型。接下來，您將學習依賴型的類型理論。在此之後，您將探索 Idris 程式語言，並通過實現它們來深入研究形式系統和類型檢查器的細節。

《Introduction to Dependent Types with Idris》將引導您從簡單的例子到更高級的技巧，隨著知識的增加，難度也會逐步提升。每個章節都包含一組基於所學內容的練習，以進一步鞏固您的學習。除了基礎知識外，不需要專門的數學知識，因此非常適合初學者。

您將學到什麼
- 理解 Lambda 演算和依賴型
- 獲得對函數式編程的洞察
- 使用 Idris 編寫數學證明

本書適合對象
- 程式設計師、數學家、學者以及對學習依賴型和 Lambda 演算感興趣的其他人。

Boro Sitnikovski has over ten years of experience working professionally as a software engineer. He started programming with assembly on an Intel x86 at the age of ten. While in high school, he won several prizes in competitive programming, varying from 4th, 3rd, and 1st place. He is an informatics graduate - his bachelor's thesis was titled "Programming in Haskell using algebraic data structures", and his master's thesis was titled "Formal verification of Instruction Sets in Virtual Machines". He has also published a few papers on software verification. Other research interests of his include programming languages, mathematics, logic, algorithms, and writing correct software. He is a strong believer in the open-source philosophy and contributes to various open-source projects. In his spare time, he enjoys some time off with his family.

Boro Sitnikovski擁有超過十年的軟體工程師專業經驗。他在十歲時就開始使用Intel x86組合語言進行編程。在高中期間，他在競爭性編程中獲得了幾個獎項，包括第四名、第三名和第一名。他是一位資訊學士畢業生，他的學士論文題目是「使用代數資料結構在Haskell中進行編程」，他的碩士論文題目是「虛擬機器中指令集的形式驗證」。他還發表了幾篇關於軟體驗證的論文。他的其他研究興趣包括編程語言、數學、邏輯、算法和編寫正確的軟體。他堅信開源哲學並為各種開源項目做出貢獻。在閒暇時間，他喜歡和家人一起放鬆。