r149

Author: liyishuai

lf-current/Postscript.html

@@ -50,8 +50,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 <ul class="doclist">
 <li> <b>函数式编程</b>：
 <ul class="doclist">
-<li> “声明式” 编程风格 (在不可变的数据构造上递归，
-            而非在可变的数组或指针结构上循环）
+<li> “声明式” 编程风格 (在不可变的数据构造上递归，而非在可变的数组或指针结构上循环）
 
 </li>
 <li> 高阶函数
@@ -70,17 +69,17 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 <div class="paragraph"> </div>
 
 <ul class="doclist">
-<li> <b>逻辑</b>, 软件工程的数学基础：
+<li> <b>逻辑</b>，软件工程的数学基础：
 <pre>
-          逻辑               微积分
-        --------   ~   -----------------
-        软件工程       机械工程/土木工程
+           逻辑                微积分
+        ---------   ~   ------------------
+         软件工程          机械工程/土木工程
 </pre>
 
 <div class="paragraph"> </div>
 
 <ul class="doclist">
-<li> 递归定义的集合，关系
+<li> 归纳定义的集合和关系
 
 </li>
 <li> 归纳证明
@@ -99,7 +98,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 <div class="paragraph"> </div>
 
 <ul class="doclist">
-<li> <b>Coq</b>, 一个工业级的证明助理
+<li> <b>Coq</b>，一个强有力的证明辅助工具
 <ul class="doclist">
 <li> 函数式核心语言
 
@@ -135,9 +134,9 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 
 
 </li>
-<li> <b>已验证的函数式算法</b>《软件基础》第三卷，Andrew Appel 著）
-             建立在 Coq 程序验证和函数式编程基础之上，
-             讨论了一般数据结构课程中的一系列主题并着眼于其形式化验证。 
+<li> <b>函数式算法验证</b>（《软件基础》第三卷，Andrew Appel 著）
+             在使用 Coq 进行程序验证和函数式编程的基础之上，
+             讨论了一般数据结构课程中的一系列主题并着眼于其形式化验证。
 </li>
 </ul>
 
@@ -148,7 +147,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 
 <div class="paragraph"> </div>
 
- 对欲求不满的人...
+ 进一步学习的资源……
 
 <div class="paragraph"> </div>
 
@@ -181,7 +180,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
               （《Real World Haskell 中文版》<a href="http://cnhaskell.com/"><span class="inlineref">http://cnhaskell.com/</span></a>）
 
 </li>
-<li> ...以及其它关于 Haskell、OCaml、 Scheme、Racket、Scala、F sharp
+<li> ……以及其它关于 Haskell、OCaml、 Scheme、Racket、Scala、F sharp
               等语言的优秀书籍。
 
 <div class="paragraph"> </div>
@@ -215,7 +214,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 
 
 </li>
-<li> 关于使用 Coq 构建已验证的系统，可以参考 2017 年 DeepSpec
+<li> 关于使用 Coq 构建形式化验证的系统，可以参考 2017 年 DeepSpec
          夏令营的课程与相关资料。
          <a href="https://deepspec.org/event/dsss17/index.html"><span class="inlineref">https://deepspec.org/event/dsss17/index.html</span></a>
 

lf-current/Postscript.v

@@ -8,25 +8,24 @@
 (** 到目前为止，我们已经学习了很多内容。我们来快速地回顾一下：
 
    - _'函数式编程'_：
-          - “声明式” 编程风格 (在不可变的数据构造上递归，
-            而非在可变的数组或指针结构上循环）
+          - “声明式” 编程风格 (在不可变的数据构造上递归，而非在可变的数组或指针结构上循环）
           - 高阶函数
           - 多态 *)
 
 (**
-     - _'逻辑'_, 软件工程的数学基础：
+     - _'逻辑'_，软件工程的数学基础：
 
-          逻辑               微积分
-        --------   ~   -----------------
-        软件工程       机械工程/土木工程
+           逻辑                微积分
+        ---------   ~   ------------------
+         软件工程          机械工程/土木工程
 
 
-          - 递归定义的集合，关系
+          - 归纳定义的集合和关系
           - 归纳证明
           - 证明对象 *)
 
 (**
-     - _'Coq'_, 一个工业级的证明助理
+     - _'Coq'_，一个强有力的证明辅助工具
           - 函数式核心语言
           - 核心策略
           - 自动化
@@ -41,14 +40,14 @@
              覆盖了了关于编程语言理论方面的研究生课程，包括霍尔逻辑
              （Hoare logic）、操作语义以及类型系统。
 
-           - _'已验证的函数式算法'_《软件基础》第三卷，Andrew Appel 著）
-             建立在 Coq 程序验证和函数式编程基础之上，
-             讨论了一般数据结构课程中的一系列主题并着眼于其形式化验证。 *)
+           - _'函数式算法验证'_（《软件基础》第三卷，Andrew Appel 著）
+             在使用 Coq 进行程序验证和函数式编程的基础之上，
+             讨论了一般数据结构课程中的一系列主题并着眼于其形式化验证。*)
 
 (* ################################################################# *)
 (** * 其它资源 *)
 
-(** 对欲求不满的人...
+(** 进一步学习的资源……
 
        - 本书包含了一些可选章节，其中讲述的内容或许会对你有用。你可以在
          目录 或
@@ -65,7 +64,7 @@
             - Real World Haskell, by Bryan O'Sullivan, John Goerzen,
               and Don Stewart [O'Sullivan 2008] (in Bib.v).
               （《Real World Haskell 中文版》http://cnhaskell.com/）
-            - ...以及其它关于 Haskell、OCaml、 Scheme、Racket、Scala、F sharp
+            - ……以及其它关于 Haskell、OCaml、 Scheme、Racket、Scala、F sharp
               等语言的优秀书籍。
 
        - 更多 Coq 相关的资源：
@@ -78,7 +77,7 @@
        - 如果你有兴趣了解现实世界中形式化验证对关键软件的应用，
          可以参阅_'《编程语言基础》'_的后记。
 
-       - 关于使用 Coq 构建已验证的系统，可以参考 2017 年 DeepSpec
+       - 关于使用 Coq 构建形式化验证的系统，可以参考 2017 年 DeepSpec
          夏令营的课程与相关资料。
          https://deepspec.org/event/dsss17/index.html
 *)