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
176/13//6 (Cit) missing early simulation citations Peter Sewell
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
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
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."