-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPreface.html
278 lines (216 loc) · 14 KB
/
Preface.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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
<!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>Preface</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="page">
<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
<li class='section_name'><a href='toc.html'>Table of Contents</a></li>
<li class='section_name'><a href='coqindex.html'>Index</a></li>
<li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
<div id="main">
<h1 class="libtitle">Preface</h1>
<div class="doc">
<a id="lab1"></a><h1 class="section">Welcome</h1>
<div class="paragraph"> </div>
This electronic book is a survey of basic concepts in the
mathematical study of programs and programming languages. Topics
include advanced use of the Coq proof assistant, operational
semantics, Hoare logic, and static type systems. 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 will be helpful.
<div class="paragraph"> </div>
As with all of the books in the <i>Software Foundations</i> series,
this one is one hundred percent formalized and machine-checked:
the entire text is literally a script for Coq. It is intended to
be read alongside (or inside) an interactive session with Coq.
All the details in the text are fully formalized in Coq, and most
of the exercises are designed to be worked using Coq.
<div class="paragraph"> </div>
The files are organized into a sequence of core chapters, covering
about one half semester's worth of material and organized into a
coherent linear narrative, plus a number of "offshoot" chapters
covering additional topics. All the core chapters are suitable
for both upper-level undergraduate and graduate students.
<div class="paragraph"> </div>
The book builds on the material from <i>Logical Foundations</i>
(<i>Software Foundations</i>, volume 1). It can be used together with
that book for a one-semester course on the theory of programming
languages. Or, for classes where students who are already
familiar with some or all of the material in <i>Logical
Foundations</i>, there is plenty of additional material to fill most
of a semester from this book alone.
</div>
<div class="doc">
<a id="lab2"></a><h1 class="section">Overview</h1>
<div class="paragraph"> </div>
The book develops two main conceptual threads:
<div class="paragraph"> </div>
(1) formal techniques for <i>reasoning about the properties of
specific programs</i> (e.g., the fact that a sorting function or
a compiler obeys some formal specification); and
<div class="paragraph"> </div>
(2) the use of <i>type systems</i> for establishing well-behavedness
guarantees for <i>all</i> programs in a given programming
language (e.g., the fact that well-typed Java programs cannot
be subverted at runtime).
<div class="paragraph"> </div>
Each of these is easily rich enough to fill a whole course in its
own right, and tackling both together naturally means that much
will be left unsaid. Nevertheless, we hope readers will find that
these themes illuminate and amplify each other and that bringing
them together creates a good foundation for digging into any of
them more deeply. Some suggestions for further reading can be
found in the <a href="Postscript.html"><span class="inlineref">Postscript</span></a> chapter. Bibliographic information
for all cited works can be found in the file <a href="Bib.html"><span class="inlineref">Bib</span></a>.
<div class="paragraph"> </div>
<a id="lab3"></a><h2 class="section">Program Verification</h2>
<div class="paragraph"> </div>
In the first part of the book, we introduce two broad topics of
critical importance in building reliable software (and hardware):
techniques for proving specific properties of particular
<i>programs</i> and for proving general properties of whole programming
<i>languages</i>.
<div class="paragraph"> </div>
For both of these, the first thing we need is a way of
representing programs as mathematical objects, so we can talk
about them precisely, plus ways of describing their behavior in
terms of mathematical functions or relations. Our main tools for
these tasks are <i>abstract syntax</i> and <i>operational semantics</i>, a
method of specifying programming languages by writing abstract
interpreters. At the beginning, we work with operational
semantics in the so-called "big-step" style, which leads to simple
and readable definitions when it is applicable. Later on, we
switch to a lower-level "small-step" style, which helps make some
useful distinctions (e.g., between different sorts of
nonterminating program behaviors) and which is applicable to a
broader range of language features, including concurrency.
<div class="paragraph"> </div>
The first programming language we consider in detail is <i>Imp</i>, a
tiny toy language capturing the core features of conventional
imperative programming: variables, assignment, conditionals, and
loops.
<div class="paragraph"> </div>
We study two different ways of reasoning about the properties of
Imp programs. First, we consider what it means to say that two
Imp programs are <i>equivalent</i> in the intuitive sense that they
exhibit the same behavior when started in any initial memory
state. This notion of equivalence then becomes a criterion for
judging the correctness of <i>metaprograms</i> -- programs that
manipulate other programs, such as compilers and optimizers. We
build a simple optimizer for Imp and prove that it is correct.
<div class="paragraph"> </div>
Second, we develop a methodology for proving that a given Imp
program satisfies some formal specifications of its behavior. We
introduce the notion of <i>Hoare triples</i> -- Imp programs annotated
with pre- and post-conditions describing what they expect to be
true about the memory in which they are started and what they
promise to make true about the memory in which they terminate --
and the reasoning principles of <i>Hoare Logic</i>, a domain-specific
logic specialized for convenient compositional reasoning about
imperative programs, with concepts like "loop invariant" built in.
<div class="paragraph"> </div>
This part of the course is intended to give readers a taste of the
key ideas and mathematical tools used in a wide variety of
real-world software and hardware verification tasks.
<div class="paragraph"> </div>
<a id="lab4"></a><h2 class="section">Type Systems</h2>
<div class="paragraph"> </div>
Our other major topic, covering approximately the second half of
the book, is <i>type systems</i> -- powerful tools for establishing
properties of <i>all</i> programs in a given language.
<div class="paragraph"> </div>
Type systems are the best established and most popular example of
a highly successful class of formal verification techniques known
as <i>lightweight formal methods</i>. These are reasoning techniques
of modest power -- modest enough that automatic checkers can be
built into compilers, linkers, or program analyzers and thus be
applied even by programmers unfamiliar with the underlying
theories. Other examples of lightweight formal methods include
hardware and software model checkers, contract checkers, and
run-time monitoring techniques.
<div class="paragraph"> </div>
This also completes a full circle with the beginning of the book:
the language whose properties we study in this part, the <i>simply
typed lambda-calculus</i>, is essentially a simplified model of the
core of Coq itself!
</div>
<div class="doc">
<a id="lab5"></a><h2 class="section">Further Reading</h2>
<div class="paragraph"> </div>
This text is intended to be self contained, but readers looking
for a deeper treatment of particular topics will find some
suggestions for further reading in the <a href="Postscript.html"><span class="inlineref">Postscript</span></a>
chapter.
</div>
<div class="doc">
<a id="lab6"></a><h1 class="section">Practicalities</h1>
<a id="lab7"></a><h2 class="section">Recommended Citation Format</h2>
<div class="paragraph"> </div>
If you want to refer to this volume in your own writing, please
do so as follows:
<br/>
<span class="inlinecode"> @<span class="id" title="var">book</span> {<span class="id" title="var">Pierce</span>:<span class="id" title="var">SF<sub>2</sub></span>,<br/>
<span class="id" title="var">author</span> = {<span class="id" title="var">Benjamin</span> <span class="id" title="var">C</span>. <span class="id" title="var">Pierce</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Arthur</span> <span class="id" title="var">Azevedo</span> <span class="id" title="var">de</span> <span class="id" title="var">Amorim</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Chris</span> <span class="id" title="var">Casinghino</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Marco</span> <span class="id" title="var">Gaboardi</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Michael</span> <span class="id" title="var">Greenberg</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">C</span>ă<span class="id" title="var">t</span>ă<span class="id" title="var">lin</span> <span class="id" title="var">Hri</span>ţ<span class="id" title="var">cu</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Vilhelm</span> <span class="id" title="var">Sjöberg</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Andrew</span> <span class="id" title="var">Tolmach</span> <span class="id" title="var">and</span><br/>
<span class="id" title="var">Brent</span> <span class="id" title="var">Yorgey</span>},<br/>
<span class="id" title="var">editor</span> = {<span class="id" title="var">Benjamin</span> <span class="id" title="var">C</span>. <span class="id" title="var">Pierce</span>},<br/>
<span class="id" title="var">title</span> = "Programming Language Foundations",<br/>
<span class="id" title="var">series</span> = "Software Foundations",<br/>
<span class="id" title="var">volume</span> = "2",<br/>
<span class="id" title="var">year</span> = "2024",<br/>
<span class="id" title="var">publisher</span> = "Electronic textbook",<br/>
<span class="id" title="var">note</span> = {<span class="id" title="var">Version</span> 6.6,<br/>
\<span class="id" title="var">URL</span>{<span class="id" title="var">http</span>://<span class="id" title="var">softwarefoundations.cis.upenn.edu</span>} },<br/>
}
</span>
</div>
<div class="doc">
<a id="lab8"></a><h1 class="section">Note for Instructors</h1>
<div class="paragraph"> </div>
If you plan to use these materials in your own course, you will
undoubtedly find things you'd like to change, improve, or add.
Your contributions are welcome! Please see the <a href="https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html"><span class="inlineref">Preface</span></a>
to <i>Logical Foundations</i> for instructions.
</div>
<div class="doc">
<a id="lab9"></a><h1 class="section">Thanks</h1>
<div class="paragraph"> </div>
Development of the <i>Software Foundations</i> series has been
supported, in part, by the National Science Foundation under the
NSF Expeditions grant 1521523, <i>The Science of Deep
Specification</i>.
</div>
<div class="code">
<span class="comment">(* 2024-08-25 08:25 *)</span><br/>
</div>
</div>
<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>