Errata

Sep. 2021
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
doi, abstract, external link, local copy, video, slides, errata
September 13, 2021
BibTeX citation
@phdthesis{sterling:2021:thesis,
  author = {Sterling, Jonathan},
  school = {Carnegie Mellon University},
  year = {2021},
  doi = {10.5281/zenodo.6990769},
  note = {Version 1.1, revised May 2022},
  number = {CMU-CS-21-142},
  title = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory},
}

A mathematical error in this dissertation was discovered by Thierry Coquand and Daniel Gratzer in April 2022 in my adaptation of Sterling and Angiuli's normalization proof for cubical type theory to support universes: the computability and normalization structures for stabilized neutral types were ill-defined, and (relatedly) the definition of the normal forms for neutral types was incorrect.

The root of the error was that the normalization struture for a stabilized neutral type did not extend its stabilization data as required. A corrected account for type theory without Kan operations was proposed by Coquand and Gratzer, and it posed no difficulties to apply this solution to full cubical type theory. The current version of this dissertation contains the needful corrections which suffice to fully recover the claimed results.

My sincere thanks to Thierry and Daniel.

JACM
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
J. Sterling and R. Harper
Journal of the ACM
doi, abstract, arXiv preprint, local copy, errata
May 2021
BibTeX citation
@article{sterling-harper:2021,
  author = {Sterling, Jonathan and Harper, Robert},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  year = {2021},
  month = oct,
  doi = {10.1145/3474834},
  eprint = {2010.08599},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
  issn = {0004-5411},
  journal = {Journal of the ACM},
  number = {6},
  title = {Logical Relations as Types: Proof-Relevant Parametricity for Program Modules},
  volume = {68},
}

After going to press, we have fixed the following mistakes:

  1. In the definition of a logos, we mistakenly said that "colimits commute with finite limits" but we meant to say that they are preserved by pullback. We thank Sarah Rovner-Frydman for noticing this mistake.
  2. In Remark 5.15, we used the notation for the closed immersion prior to introducing it.
  3. We have fixed a few broken links in the bibliography.

The local copy linked here has the corrections implemented.