Programming language foundations in Agda
Programming language foundations in Agda
复制标题
Agda 编程语言基础
DOI：
10.1016/j.scico.2020.102440
复制
发表时间：
2020
影响因子：
1.3
通讯作者：
Wadler, Philip
中科院分区：
文献类型：
--
作者：
Kokke, Wen;Siek, Jeremy G.;Wadler, Philip
关于形式化方法的主要教科书之一是软件基础（SF），由Benjamin Pierce与其他人合作编写，并基于Coq。在课堂上使用了五年后，我们得出的结论是，Coq并不是实现这一目的的最佳工具，因为太多的课程需要专注于学习证明推导的策略，以学习编程语言理论为代价。因此，我们编写了一本新的教科书，编程语言基础在Agda（PLFA）。PLFA涵盖了与SF相同的领域，尽管它不是一个盲目的模仿。我们从编写PLFA中学到了什么？首先，这是可能的。有人可能会认为，如果没有证明策略，证明就会变得太长，但事实上，PLFA中的证明与SF中的证明长度大致相同。Coq中的证明需要一个交互环境才能理解，而Agda中的证明可以在页面上阅读。第二，保存和进展的建设性证据会立即产生原型评估者。回顾过去，这一事实是显而易见的，但科幻小说并没有利用它（相反，科幻小说提供了一种单独的规范化策略），我们也无法在文学作品中找到它。第三，使用外部类型的术语远不如使用内部类型的术语明显。顺丰采用前者，而PLFA采用两者；前者使用的Agda代码行数大约是后者的1.6行，大致是黄金比例。教科书是用Agda文字编写的，可以在这里找到：http://plfa.inf.ed.ac.uk
One of the leading textbooks for formal methods isSoftware Foundations(SF), written by Benjamin Pierce in collaboration with others, and based on Coq. After five years using SF in the classroom, we came to the conclusion that Coq is not the best vehicle for this purpose, as too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning programming language theory. Accordingly, we have written a new textbook,Programming Language Foundations in Agda(PLFA). PLFA covers much of the same ground as SF, although it is not a slavish imitation.What did we learn from writing PLFA? First, that it is possible. One might expect that without proof tactics that the proofs become too long, but in fact proofs in PLFA are about the same length as those in SF. Proofs in Coq require an interactive environment to be understood, while proofs in Agda can be read on the page. Second, that constructive proofs of preservation and progress give immediate rise to a prototype evaluator. This fact is obvious in retrospect but it is not exploited in SF (which instead provides a separate normalise tactic) nor can we find it in the literature. Third, that using extrinsically-typed terms is far less perspicuous than using intrinsically-typed terms. SF uses the former presentation, while PLFA presents both; the former uses about 1.6 as many lines of Agda code as the latter, roughly the golden ratio.The textbook is written as a literate Agda script, and can be found here: http://plfa.inf.ed.ac.uk