Type Theory and Formal Proof: An Introduction (Hardcover)

Rob Nederpelt, Herman Geuvers

  • 出版商: Cambridge
  • 出版日期: 2014-11-06
  • 售價: $3,360
  • 貴賓價: 9.8$3,293
  • 語言: 英文
  • 頁數: 466
  • 裝訂: Hardcover
  • ISBN: 110703650X
  • ISBN-13: 9781107036505
  • 相關分類: 程式語言邏輯設計 Logic-design
  • 立即出貨 (庫存=1)

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

商品描述

Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems, including the well-known and powerful Calculus of Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalise mathematics. The only prerequisite is a basic knowledge of undergraduate mathematics. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarise themselves with the material.

商品描述(中文翻譯)

類型理論是一個快速發展的領域,處於邏輯、計算機科學和數學的交叉路口。這本溫和的逐步介紹對於需要理解數學機械的內部運作、邏輯規則的角色、定義的重要貢獻以及良好結構證明的決定性本質的研究生和研究人員來說是理想的。作者從無類型的λ演算開始,然後介紹了幾個基本的類型系統,包括著名而強大的構造演算法。本書還涵蓋了證明檢查和證明開發的本質,以及使用依賴類型理論來形式化數學。唯一的先決條件是基本的本科數學知識。精心選擇的例子貫穿整個理論。每章結束時都有內容摘要、一些歷史背景、進一步閱讀建議和一些練習題,以幫助讀者熟悉材料。