类型和程序设计语言
类型和程序设计语言内容简介
类型理论在程序设计语言的发展中起着举足轻重的作用，成熟的类型系统可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。 要理解类型系统在程序设计语言中发挥的作用，本书将是首选读物。本书内容覆盖基本操作语义及其相关证明技巧、无类型lambda演算、简单类型系统、全称多态和存在多态、类型重构、子类型化、囿界量词、递归类型、类型算子等内容。本书既注重内容的广度，也注重内容的深度，实用性强。在引入语言的语法对象时先举例，然后给出形式定义及基本证明，在对理论的进一步研究后给出了类型检查算法，并对每种算法都给出了OCaml程序的具体实现。本书对类型理论中的概念都有详细的阐述，为读者提供了一个进一步理论学习的基础。本书内容广泛，读者可以根据自己的需要有选择地深入阅读。 本书适合从事程序设计的研究人员和开发人员，以及程序设计语言和类型理论的研究人员阅读。可作为计算机专业高年级学生、研究生的学习教材。
热门摘录
Q: Why bother doing proofs about programming languages? They are almost always boring if the definitions are right. A: The definitions are almost always wrong.
At the other end are techniques of much more modest power—modest enough that automatic checkers can be built into compilers, linkers, or program analyzers
The more abstract focuses on connections between various “pure typed lambda-calculi” and varieties of logic, via the Curry-Howard correspondence
they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence,
type systems are also used to enforce higher-level modularity properties and to protect the in- tegrity of user-defined abstractions.
Chains can be either finite or infinite, but we are more interested in infinite ones, as in the next definition
The mathemati- cal foundations of inductive reasoning will be considered in more detail in Chapter 21, where we will see that all these specific induction principles are instances of a single deeper idea.
lambda演算是Alonzo Church于20世纪20年代发明的一个形式系统，其中所有的计算规约为函数定义和应用的基本运算。 lambda演算广泛用于程序语言特征的说明、语言设计和实现，以及类型系统的研究。他的重要性在于，既可以作为描述计算的一个简单程序语言，同时也可以作为一个数学对象，其中严格语句能够得到证明。
To build a new array, we allocate a reference cell and fill it with a function that, when given an index, always returns 0.
To look up an element of an array, we simply apply the function to the desired index.
The typing rules for ref, :=, and ! follow straightforwardly from the behaviors we have given them.
形式方法只有到了不理解它何的人们都能使用时才会产生重大影响。
类型和程序设计语言书评
还没人写过点评，快来抢沙发吧
