Introduction to Dependent Types with Idris: Encoding Program Proofs in Types
暫譯: 依賴型別入門：使用 Idris 在型別中編碼程式證明

Sitnikovski, Boro

Introduction to Dependent Types with Idris: Encoding Program Proofs in Types
  • 出版商: Apress
  • 出版日期: 2023-03-18
  • 售價: $1,350
  • 貴賓價: 9.5 折 $1,283
  • 語言: 英文
  • 頁數: 157
  • 裝訂: Quality Paper - also called trade paper
  • ISBN: 1484292588
  • ISBN-13: 9781484292587

    • 海外代購書籍(需單獨結帳)

相關主題

商品描述

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.

商品描述(中文翻譯)

依賴類型（Dependent types）是一個概念，允許開發者撰寫帶有證明的程式碼。Idris 是一種支援依賴類型的程式語言。本書將教您 Idris 的數學基礎，以及如何使用它來撰寫軟體並數學證明屬性。

本書的第一部分作為對語言底層理論的介紹。它首先回顧形式系統和數學邏輯系統作為基礎構建塊，然後逐步建立到依賴類型。接下來，您將學習依賴類型的類型理論。隨後，您將探索 Idris 程式語言，並通過實現它們來深入探討形式系統和類型檢查器。

使用 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 程式設計」，碩士論文題目為「虛擬機中指令集的形式驗證」。他還發表了一些有關軟體驗證的論文。他的其他研究興趣包括程式語言、數學、邏輯、演算法以及撰寫正確的軟體。他堅信開源哲學，並為各種開源專案做出貢獻。在空閒時間，他喜歡與家人共度時光。

類似商品