-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathindex.html
146 lines (129 loc) · 5.2 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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
<!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>Software Foundations</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>The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable
software.</strong></p>
<p>The principal novelty of the series is that every detail is one hundred
percent formalized and machine-checked: the entire text of each volume,
including the exercises, is literally a "proof script" for the Coq
proof assistant.
</p>
<p>The exposition is intended for a broad range of readers, from advanced
undergraduates to PhD students and researchers. No specific background in
logic or programming languages is assumed, though a degree of mathematical
maturity is helpful. A one-semester course can expect to cover <i>Logical
Foundations</i> plus most of <i>Programming Language
Foundations</i> or <i>Verified Functional Algorithms</i>, or selections
from both.</p>
<div style="margin-top:30px;">
<div class='column pub'>
<table class="logical">
<tr>
<td class="tab">Volume 1</td>
</tr>
<tr>
<td>
<p><i>Logical Foundations</i> is the entry-point to the series. It covers
functional programming, basic concepts of logic, computer-assisted theorem
proving, and Coq.</p>
<a href="lf-current/index.html"><img src="common/media/image/lf_icon.jpg" width="200px" /></a>
</td>
</tr>
</table>
</div>
<div class='column pub'>
<table class="language_found">
<tr>
<td class="tab">Volume 2</td>
</tr>
<tr>
<td>
<p><i>Programming Language Foundations</i> surveys the theory of programming languages, including
operational semantics, Hoare logic, and static type systems.</p>
<a href="plf-current/index.html"><img src="common/media/image/plf_icon.jpg" width="200px" /></a>
</td>
</tr>
</table>
</div>
<div class='column pub'>
<table class="algo">
<tr>
<td class="tab">Volume 3</td>
</tr>
<tr>
<td>
<p><i>Verified Functional Algorithms</i> shows how a variety of fundamental
data structures can be specified and mechanically verified.<br/><br/></p>
<a href="vfa-current/index.html"><img src="common/media/image/vfa_icon.jpg" width="200px"></a>
</td>
</tr>
</table>
</div>
<div class='column pub'>
<table class="qc">
<tr>
<td class="tab">Volume 4</td>
</tr>
<tr>
<td>
<p><i>QuickChick: Property-Based Testing in Coq</i>
introduces tools for combining randomized
property-based testing with formal
specification and proof in the Coq ecosystem.</p>
<a href="qc-current/index.html"><img src="common/media/image/qc_icon.jpg" width="200px"></a>
</td>
</tr>
</table>
</div>
<div class='column pub'>
<table class="vc">
<tr>
<td class="tab">Volume 5</td>
</tr>
<tr>
<td>
<p><i>Verifiable C</i> is an extended hands-on tutorial on specifying and
verifying real-world C programs using the Princeton Verified Software
Toolchain.<br/><br/></p>
<a href="vc-current/index.html"><img src="common/media/image/vc-icon.png" width="200px"></a>
</td>
</tr>
</table>
</div>
<div class='column pub'>
<table class="slf">
<tr>
<td class="tab">Volume 6</td>
</tr>
<tr>
<td>
<p><i>Separation Logic Foundations</i> is an in-depth
introduction to separation logic—a practical approach to
modular verification of imperative programs—and how
to build program verification
tools on top of it.<br/><br/></p>
<a href="slf-current/index.html"><img src="common/media/image/slf-icon.png" width="200px"></a>
</td>
</tr>
</table>
</div>
</div>
</div>
</div>
<div id="main_home">
<div id="index_content">
</div>
</div>
</body>
</html>