← 黑客书架

具体语义学

Concrete Semantics

Tobias Nipkow, Gerwin Klein · 初版 2014 年

  • 5次提及
  • 4人推荐
  • 5位 HN 评论者

简介

本书第一部分是对 Isabelle 证明助手实践应用的入门介绍。它将指导你如何编写函数式程序和归纳定义，以及如何在 Isabelle 的结构化证明语言中证明它们的性质。第二部分是对命令式语言语义的介绍，重点关注编译器和程序分析器等应用。其最显著的特色在于所有数学内容均已在 Isabelle 中实现形式化，且大部分是可执行的。第一部分侧重于 Isabelle 中的证明细节；第二部分即便对前者不甚熟悉也可以阅读

Hacker News 读者推荐

另一本很棒的书是：* Nipkow 和 Klein 写的《Concrete Semantics》http://concrete-semantics.org/，它也是 Isabelle/HOL 证明助手的入门教材，并在 Isabelle 中对所有编程语言（PL）内容进行了形式化。还有：* 《Semantics with…

tom_mellior 在 HN 的推荐

……* http://www.cs.man.ac.uk/~pt/Practical_Foundations/ * https://www.mta.ca/~rrosebru/setsformath/ * https://github.com/ademinn/ttfv/blob/master/2006.%20Sorensen... * http://www21.in.tum.de/~nipkow/Concrete-Semantics/ * http://adam.chlipala.net/frap/ * https://softwarefoundations.cis.upenn.edu/

hellerup89 在 HN 的推荐

……另外 3 本是经典，但要硬核得多（比如 Nielson 夫妇的那本书需要相当扎实的抽象代数背景）：* Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/ * Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/ * FRAP (Chlipala): http://adam.chlipala.net/frap/ * Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking *……

nextos 在 HN 的推荐

找书

豆瓣 微信读书 京东 Open Library

在黑客书架打开完整页面 →

数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。