-
Notifications
You must be signed in to change notification settings - Fork 0
/
qed_errata.html
181 lines (181 loc) · 9.39 KB
/
qed_errata.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
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="generator" content="pandoc" />
<title>Errata for QED at Large</title>
<style type="text/css">code{white-space: pre;}</style>
</head>
<body>
<div id="header">
<h1 class="title">Errata for QED at Large</h1>
</div>
<p>The table below contains corrections to the original manuscript. When further explanation is warranted, it is provided below the table, and linked to within the first column. Pending additions to the errata can be found in <a href="https://github.com/proofengineering/proofengineering.github.io/issues">Github issues</a>.</p>
<p>A note on omissions: The survey paper often lists a non-exhaustive sample of work in a domain. This is to some degree necessary. Still, this page lists omissions as relevant, especially when particularly influential work is missing or when sampled work is biased toward particular interactive theorem provers.</p>
<h1 id="corrections">Corrections</h1>
<p>Page references are for printed line numbers (in the range 103 to 281).</p>
<p>Abbreviations for different types of corrections:</p>
<ul>
<li>Cor - correction of language</li>
<li>Cpltf - change of page layout or text format</li>
<li>Fct - factual correction</li>
<li>Cit - correction or addition of citation</li>
<li>Cod - correction of code</li>
<li>Clar - clarification</li>
</ul>
<table>
<thead>
<tr class="header">
<th align="left">Page/Line/Footnote/Explanation</th>
<th align="left">Original text</th>
<th align="left">(type of correction) Corrected text</th>
<th align="left">Acknowledgement</th>
</tr>
</thead>
<tbody>
<tr class="odd">
<td align="left">108/16//</td>
<td align="left">"... a <em>regular language</em> ..."</td>
<td align="left">(Fct) "... a <em>language</em> ..."</td>
<td align="left">Virgil Serbanuta</td>
</tr>
<tr class="even">
<td align="left">112/18//<a href="#exp5">5</a></td>
<td align="left"></td>
<td align="left">(Cit) missing CompCertTSO and Crellvm</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="odd">
<td align="left">121/17//</td>
<td align="left">"For example, mst papers ..."</td>
<td align="left">(Cor) "For example, most papers ... "</td>
<td align="left">Mukesh Tiwari</td>
</tr>
<tr class="even">
<td align="left">135/1//<a href="#exp4">4</a></td>
<td align="left"></td>
<td align="left">(Cit) missing early work on definitional mechanisms in HOL</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="odd">
<td align="left">154/27//</td>
<td align="left">"mush = ..."</td>
<td align="left">(Cod) <a href="http://github.com/proofengineering/proofengineering.github.io/issues/4">see code fix</a></td>
<td align="left">Joomy Korkut</td>
</tr>
<tr class="even">
<td align="left">163/22//<a href="#exp3">3</a></td>
<td align="left">"Note that the extra spacing is necessary ... "</td>
<td align="left">(Fct) omit---inaccurate</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="odd">
<td align="left">163/24//</td>
<td align="left">"The more general proof assistant-agnostic specification language Lem"</td>
<td align="left">(Fct) "The proof assistant-agnostic specification language Lem"</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="even">
<td align="left">163/30//</td>
<td align="left"></td>
<td align="left">(Cit) missing citation for <a href="http://www.specware.org/">Specware</a> in refinement</td>
<td align="left">Matthew Wilson</td>
</tr>
<tr class="odd">
<td align="left">164/9//</td>
<td align="left">"This relation can also be stated and proven ... "</td>
<td align="left">(Clar) "This relation can also be proven ... "</td>
<td align="left">Tej Chajed</td>
</tr>
<tr class="even">
<td align="left">164/30//</td>
<td align="left"></td>
<td align="left">(Clar) It is a stretch to include proof and program refinement in the same section</td>
<td align="left">Tej Chajed</td>
</tr>
<tr class="odd">
<td align="left">170/1//</td>
<td align="left">"more the more"</td>
<td align="left">(Cor) "the more"</td>
<td align="left">Christoph Baumann</td>
</tr>
<tr class="even">
<td align="left">176/13//<a href="#exp6">6</a></td>
<td align="left"></td>
<td align="left">(Cit) missing early simulation citations</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="odd">
<td align="left">176/16//<a href="#exp8">8</a></td>
<td align="left"></td>
<td align="left">(Clar) CompCert simulation terminology is confusing (see note) </td>
<td align="left">Tej Chajed</td>
</tr>
<tr class="even">
<td align="left">176/30//<a href="#exp7">7</a></td>
<td align="left">"Together, a forward and a backward simulation establish indistinguishability"</td>
<td align="left">(Fct) not always---see note</td>
<td align="left">Peter Sewell</td>
</tr>
<tr class="odd">
<td align="left">179/18//</td>
<td align="left">"defied"</td>
<td align="left">(Cor) "defined"</td>
<td align="left">Anton Trunov</td>
</tr>
<tr class="even">
<td align="left">182/19//</td>
<td align="left">"his can"</td>
<td align="left">(Cor) "this can"</td>
<td align="left">Christoph Baumann</td>
</tr>
<tr class="odd">
<td align="left">183/30//</td>
<td align="left">"dedicate"</td>
<td align="left">(Cor) "dedicated"</td>
<td align="left">Anton Trunov</td>
</tr>
<tr class="even">
<td align="left">184/28//<a href="#exp1">1</a></td>
<td align="left"></td>
<td align="left">(Cit) missing citation for universe polymorphism</td>
<td align="left">Bob Harper</td>
</tr>
<tr class="odd">
<td align="left">190/15//<a href="#exp2">2</a></td>
<td align="left"></td>
<td align="left">(Cit) missing citations for cubical type theory</td>
<td align="left">Bob Harper</td>
</tr>
<tr class="even">
<td align="left">191/27//</td>
<td align="left"></td>
<td align="left">(Clar) "REPL" is first used here, but defined later on page 196</td>
<td align="left">Christoph Baumann</td>
</tr>
<tr class="odd">
<td align="left">194/21//</td>
<td align="left">"... is an underaddressed tenant POPLMark"</td>
<td align="left">(Cor) "... is an underaddressed tenet of POPLMark"</td>
<td align="left">Christoph Baumann</td>
</tr>
<tr class="even">
<td align="left">238/2//</td>
<td align="left">"The End of History:"</td>
<td align="left">(Cit) "The End of History?"</td>
<td align="left">Anton Trunov</td>
</tr>
</tbody>
</table>
<h1 id="explanations">Explanations</h1>
<p><a name="exp1">1</a>: The universe polymorphism algorithm in Coq that we cite is based on <a href="https://doi.org/10.1016/0304-3975(90)90108-T">Type Checking with Universes</a> by Robert Harper and Randy Pollack. The DOI that we link to was published in 1991, though the algorithm surfaced in a draft from 1989 that is also available online <a href="https://doi.org/10.1007/3-540-50940-2_39">here</a>.</p>
<p><a name="exp2">2</a>: There are at least two flavors of cubical type theory, and we cite only one. The missing citation can be found in <a href="https://doi.org/10.1145/3009837.3009861">Computational Higher-Dimensional Type Theory</a> by Carlo Angiuli, Robert Harper, and Todd Wilson.</p>
<p><a name="exp3">3</a>: From Peter: "The grammar productions need spacing between tokens, to let Ott infer what the tokens are, but that spacing is not needed in the symbolic terms in inductive rules."</p>
<p><a name="exp4">4</a>: See, for example, <a href="https://doi.org/10.1007/BF01383982">The HOL Logic Extended with Quantification over Type Variables</a> by Thomas F. Melham, and <a href="https://doi.org/10.1109/hol.1991.596299">A Package For Inductive Relation Definitions In HOL</a>, also by Thomas F. Melham.</p>
<p><a name="exp5">5</a>: For CompCertTSO, see <a href="https://doi.org/10.1007/978-3-642-23702-7_14">Verifying Fence Elimination Optimisations</a> by Viktor Vafeiadis and Francesco Zappa Nardelli, <a href="https://doi.org/10.1145/1926385.1926393">Relaxed-Memory Concurrency and Verified Compilation</a> by Jaroslav Ŝevčik <em>et al.</em>, and <a href="https://doi.org/10.1145/2487241.2487248">CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency</a> by Jaroslav Ŝevčik <em>et al.</em> For Crellvm, see <a href="https://doi.org/10.1145/3192366.3192377">Crellvm: Verified Credible Compilation for LLVM</a> by Jeehoon Kang <em>et al.</em></p>
<p><a name="exp6">6</a>: We cite a tech report explaining simulation when we introduce the concept, but this dates back at least to Milner's <a href="https://dl.acm.org/citation.cfm?id=539036">process calculus</a> work more than a decade before the cited report.</p>
<p><a name="exp7">7</a>: The coverage of simulation in this survey is a bit simplified. Much of the simulation literature defines simulation in terms of <em>observable behavior</em>. The truth of this particular comment about indistinguishability depends on the definition of "observable behavior."</p>
<p><a name="exp8">8</a>: The term "backward simulation" as used by CompCert is not the same as "backward simulation" as used by other sources like the cited tech report and <a href="https://web.mit.edu/6.826/www/notes/HO8.pdf">Butler Lampson's lecture notes</a>. In those sources, "backward simulation" refers to induction in reverse execution order.</p>
</body>
</html>