Skip to content
Permalink
master
Switch branches/tags
Go to file
 
 
Cannot retrieve contributors at this time
title
Errata for QED at Large

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.

Corrections

Page references are for printed line numbers (in the range 103 to 281).

Abbreviations for different types of corrections:

  • Cor - correction of language
  • Cpltf - change of page layout or text format
  • Fct - factual correction
  • Cit - correction or addition of citation
  • Cod - correction of code
  • Clar - clarification
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

Explanations

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.