函数式程序设计入门讲义

Posted 2021-05-08 形式化方法研究与实践

内容简介：

近年来形式化验证方法逐渐受到关注，函数式语言被广泛用于开发编译器、程序分析器、定理证明器，以帮助验证软硬件系统的功能正确性。在这样的背景下，作者认为有必要推广函数式程序设计相关的教学工作，因而编写了这本简明讲义，作为学习函数式程序设计的入门读物。在内容选取上，本讲义只涉及λ-演算，Coq和OCaml。第一章介绍不带类型的λ-演算和简单类型的λ-演算，主要讨论语法和β-规约语义。第二章从函数式编程的角度介绍Coq，内容涉及基本数据类型、多态数据结构、高阶函数以及柯里-霍华德关联。作者认为Coq是来用于讲授归纳定义和归纳证明思想的出色工具。第三章介绍一门通用的编程语言OCaml，除了基本的程序设计概念，还讨论函子和Monad这样比较高级的特征。第四章提供了部分习题的参考答案，以方便感兴趣的读者自行学习。本讲义可作为高等院校计算机科学和软件工程专业的本科教学参考书。

 

作者简介：

邓玉欣，华东师范大学软件工程学院教授。长期从事形式化方法领域的基础研究，主要研究方向包括并发计算模型和程序理论。代表性工作包括一个已经被国外学者写进教科书的“邓引理”(DengLemma)（R.Gorrieri, C. Versari. Introduction to Concurrency Theory – Transition Systemsand CCS. Springer, 2015）和关于概率并发理论的一部英文专著（Y.Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer,2015）。发表学术论文75篇, 其中45篇为第一作者，单篇最高引用118次(GoogleScholar)。多篇论文发表在国际权威期刊和会议如Informationand Computation、TheoreticalComputer Science、CONCUR、ICALP、LICS、POPL等。曾为CONCUR2018作特邀报告，担任TASE2016程序委员会共同主席，多次担任理论计算机科学领域著名会议如ICALP2013、ICALP2016、ICALP2018、CONCUR2019、CAV2021的程序委员会委员。

 

https://faculty.ecnu.edu.cn/_upload/article/files/0b/e3/ed18bad24dd9b9d44a7251fc3d1c/faa8ee9a-0273-465c-80bb-10e05427f8a4.pdf