-
Notifications
You must be signed in to change notification settings - Fork 69
/
index.html
113 lines (80 loc) · 2.89 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>软件基础</title>
<!-- add to head -->
<link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">
</head>
<body class="sf_home">
<div id="page">
<div id="header">
<!-- added to header -->
<img src="common/media/image/sf_logo_lg.png" width="400px" style="padding-bottom:50px;">
<p><strong>《软件基础》系列广泛地介绍了可靠软件的数学基础。</strong></p>
<p>
本系列书籍最主要的新颖之处在于，书中的每一处细节都百分之百地形式化且通过了机器验证。
每卷书中的所有文本，包括练习，都是一份 Coq 证明助理的「证明脚本」。
</p>
<p>本系列书籍的目标受众包括从高年级本科生到博士以及研究者在内的广大读者。
书中并未假定读者有逻辑学或编程语言的背景，不过一定的数学熟练度会很有帮助。
一学期的课程可以涵盖<b>《逻辑基础》</b>加上<b>《编程语言基础》</b>或<b>《函数式算法验证》</b>中的大部分内容，
当然也可以从二者中均选取一些内容。</p>
<div style="margin-top: 60px;">
<div class='column pub'>
<table class="logical">
<tr>
<td class="tab">第一卷</td>
</tr>
<tr>
<td>
<p>《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Coq 证明助理。</p>
<a href="lf-current/index.html"><img src="common/media/image/lf_icon.jpg" width="200px"></a>
</td>
</table>
</div>
<div class='column pub'>
<table class="language_found">
<tr>
<td class="tab">第二卷</td>
</tr>
<tr>
<td>
<p>《编程语言基础》考察了编程语言理论，包括操作语义、霍尔逻辑以及静态类型系统。 </p>
<a href="plf-current/index.html"><img src="common/media/image/plf_icon.jpg" width="200px"></a>
</td>
</table>
</div>
</div>
<div class='column pub'>
<table class="algo">
<tr>
<td class="tab">第三卷</td>
</tr>
<tr>
<td>
<p>《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。</p>
<a href="vfa-current/index.html"><img src="common/media/image/vfa_icon.jpg" width="200px"></a>
</td>
</table>
</div>
<div class='column pub'>
<table class="qc">
<tr>
<td class="tab">第四卷</td>
</tr>
<tr>
<td>
<p>《QuickChick：用 Coq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Coq 生态系统中的形式化规范和证明相结合的工具和技术。</p>
<a href="qc-current/index.html"><img src="common/media/image/qc_icon.jpg" width="200px"></a>
</td>
</table>
</div>
</div>
<div id="main_home">
<div id="index_content">
</div>
</body>
</html>