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 Github issues.
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.
Page references are for printed line numbers (in the range 103 to 281).
Abbreviations for different types of corrections:
| Page/Line/Footnote/Explanation | Original text | (type of correction) Corrected text | Acknowledgement |
|---|---|---|---|
| 108/16// | "... a regular language ..." | (Fct) "... a language ..." | Virgil Serbanuta |
| 112/18//5 | (Cit) missing CompCertTSO and Crellvm | Peter Sewell | |
| 121/17// | "For example, mst papers ..." | (Cor) "For example, most papers ... " | Mukesh Tiwari |
| 135/1//4 | (Cit) missing early work on definitional mechanisms in HOL | Peter Sewell | |
| 154/27// | "mush = ..." | (Cod) see code fix | Joomy Korkut |
| 163/22//3 | "Note that the extra spacing is necessary ... " | (Fct) omit---inaccurate | Peter Sewell |
| 163/24// | "The more general proof assistant-agnostic specification language Lem" | (Fct) "The proof assistant-agnostic specification language Lem" | Peter Sewell |
| 163/30// | (Cit) missing citation for Specware in refinement | Matthew Wilson | |
| 164/9// | "This relation can also be stated and proven ... " | (Clar) "This relation can also be proven ... " | Tej Chajed |
| 164/30// | (Clar) It is a stretch to include proof and program refinement in the same section | Tej Chajed | |
| 170/1// | "more the more" | (Cor) "the more" | Christoph Baumann |
| 176/13//6 | (Cit) missing early simulation citations | Peter Sewell | |
| 176/16//8 | (Clar) CompCert simulation terminology is confusing (see note) | Tej Chajed | |
| 176/30//7 | "Together, a forward and a backward simulation establish indistinguishability" | (Fct) not always---see note | Peter Sewell |
| 179/18// | "defied" | (Cor) "defined" | Anton Trunov |
| 182/19// | "his can" | (Cor) "this can" | Christoph Baumann |
| 183/30// | "dedicate" | (Cor) "dedicated" | Anton Trunov |
| 184/28//1 | (Cit) missing citation for universe polymorphism | Bob Harper | |
| 190/15//2 | (Cit) missing citations for cubical type theory | Bob Harper | |
| 191/27// | (Clar) "REPL" is first used here, but defined later on page 196 | Christoph Baumann | |
| 194/21// | "... is an underaddressed tenant POPLMark" | (Cor) "... is an underaddressed tenet of POPLMark" | Christoph Baumann |
| 238/2// | "The End of History:" | (Cit) "The End of History?" | Anton Trunov |
1: The universe polymorphism algorithm in Coq that we cite is based on Type Checking with Universes 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 here.
2: There are at least two flavors of cubical type theory, and we cite only one. The missing citation can be found in Computational Higher-Dimensional Type Theory by Carlo Angiuli, Robert Harper, and Todd Wilson.
3: 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."
4: See, for example, The HOL Logic Extended with Quantification over Type Variables by Thomas F. Melham, and A Package For Inductive Relation Definitions In HOL, also by Thomas F. Melham.
5: For CompCertTSO, see Verifying Fence Elimination Optimisations by Viktor Vafeiadis and Francesco Zappa Nardelli, Relaxed-Memory Concurrency and Verified Compilation by Jaroslav Ŝevčik et al., and CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency by Jaroslav Ŝevčik et al. For Crellvm, see Crellvm: Verified Credible Compilation for LLVM by Jeehoon Kang et al.
6: We cite a tech report explaining simulation when we introduce the concept, but this dates back at least to Milner's process calculus work more than a decade before the cited report.
7: The coverage of simulation in this survey is a bit simplified. Much of the simulation literature defines simulation in terms of observable behavior. The truth of this particular comment about indistinguishability depends on the definition of "observable behavior."
8: 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 Butler Lampson's lecture notes. In those sources, "backward simulation" refers to induction in reverse execution order.