具体语义学
Concrete Semantics
Tobias Nipkow、Gerwin Klein · 初版 2014 年
4人推荐
5位读者提及
5次提及
本书第一部分是对 Isabelle 证明助手实践应用的入门介绍。它将指导你如何编写函数式程序和归纳定义，以及如何在 Isabelle 的结构化证明语言中证明它们的性质。第二部分是对命令式语言语义的介绍，重点关注编译器和程序分析器等应用。其最显著的特色在于所有数学内容均已在 Isabelle 中实现形式化，且大部分是可执行的。第一部分侧重于 Isabelle 中的证明细节；第二部分即便对前者不甚熟悉也可以阅读
Hacker News 上怎么说
正在加载完整评论……
另一本很棒的书是：* Nipkow 和 Klein 写的《Concrete Semantics》http://concrete-semantics.org/，它也是 Isabelle/HOL 证明助手的入门教材，并在 Isabelle 中对所有编程语言（PL）内容进行了形式化。还有：* 《Semantics with…
Another good one is: * Concrete Semantics by Nipkow and Klein http://concrete-semantics.org/, which is also an introduction to the Isabelle/HOL proof assistant and formalizes all of the PL content in Isabelle There's also: * Semantics with…
……* 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/
…* 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/
……另外 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 *……
…The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background): * 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 *…
T. Nipkow, G. Klein, 《Concrete Semantics》. http://concrete-semantics.org/ B. C. Pierce 等, 《Software Foundations》. https://softwarefoundations.cis.upenn.edu/
T. Nipkow, G. Klein, Concrete Semantics. http://concrete-semantics.org/ B. C. Pierce et al, Software Foundations. https://softwarefoundations.cis.upenn.edu/
……用 Ocaml 写的编译器）做不到。稍微通俗点说，自举（bootstrapping）降低了可信计算基（TCB）。也许 Leroy 的 [3, 4] 是学习这个领域的良好起点。[1] T. Nipkow, G. Klein, Concrete Semantics. http://www.concrete-semantics.org/ [2] A. Chlipala, A verified compiler for an impure functional language. http://adam.chlipala.net/papers/ImpurePOPL10 [3] X. Leroy, Verifying a compiler: Why? How?…
…compiler written in Ocaml) can't. Simplifying a bit, bootstrapping lowers the trusted computing base. Maybe Leroy's [3, 4] are good starting point for learning about this field. [1] T. Nipkow, G. Klein, Concrete Semantics. http://www.concrete-semantics.org/ [2] A. Chlipala, A verified compiler for an impure functional language. http://adam.chlipala.net/papers/ImpurePOPL10 [3] X. Leroy, Verifying a compiler: Why? How?…