Verified Functional Programming in Agda

Aaron Stump

  • 出版商: Morgan & Claypool
  • 出版日期: 2016-02-01
  • 售價: $2,780
  • 貴賓價: 9.5$2,641
  • 語言: 英文
  • 頁數: 284
  • 裝訂: Paperback
  • ISBN: 1970001240
  • ISBN-13: 9781970001242
  • 海外代購書籍(需單獨結帳)

買這商品的人也買了...

商品描述

Agda is an advanced programming language based on Type Theory. Agda's type system is expressive enough to support full functional verification of programs, in two styles. In external verification, we write pure functional programs and then write proofs of properties about them. The proofs are separate external artifacts, typically using structural induction. In internal verification, we specify properties of programs through rich types for the programs themselves. This often necessitates including proofs inside code, to show the type checker that the specified properties hold. The power to prove properties of programs in these two styles is a profound addition to the practice of programming, giving programmers the power to guarantee the absence of bugs, and thus improve the quality of software more than previously possible. Verified Functional Programming in Agda is the first book to provide a systematic exposition of external and internal verification in Agda, suitable for undergraduate students of Computer Science. No familiarity with functional programming or computer-checked proofs is presupposed. The book begins with an introduction to functional programming through familiar examples like booleans, natural numbers, and lists, and techniques for external verification. Internal verification is considered through the examples of vectors, binary search trees, and Braun trees. More advanced material on type-level computation, explicit reasoning about termination, and normalization by evaluation is also included. The book also includes a medium-sized case study on Huffman encoding and decoding.

商品描述(中文翻譯)

Agda是一種基於類型理論的先進程式語言。Agda的類型系統足夠表達性,可以支援對程式進行完整的功能驗證,有兩種風格。在外部驗證中,我們編寫純函數程式,然後編寫關於這些程式性質的證明。這些證明是獨立的外部工件,通常使用結構歸納。在內部驗證中,我們通過豐富的類型來指定程式的性質,這往往需要在程式碼中包含證明,以向類型檢查器證明指定的性質成立。以這兩種風格證明程式性質的能力是對程式設計實踐的深刻補充,使程式設計師能夠保證程式中不存在錯誤,從而比以前更能提高軟體的品質。《Agda中的驗證功能程式設計》是第一本系統介紹Agda中外部和內部驗證的書籍,適合計算機科學本科生閱讀。不需要對函數程式設計或計算機檢查證明有任何了解。本書從介紹函數程式設計開始,通過布林值、自然數和列表等熟悉的例子以及外部驗證技術。內部驗證通過向量、二元搜索樹和Braun樹等例子進行探討。書中還包括關於類型級計算、明確關於終止性的推理以及通過評估實現正規化的高級材料。書中還包括一個中等規模的Huffman編碼和解碼案例研究。