Errata

FSCD '22	Sheaf semantics of termination-insensitive noninterference J. Sterling and R. Harper International Conference on Formal Structures for Computation and Deduction (FSCD) doi, abstract, arXiv preprint, local copy, video, slides, errata June 28, 2022 BibTeX citation @inproceedings{sterling-harper:2022, author = {Sterling, Jonathan and Harper, Robert}, editor = {Felty, Amy P.}, address = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, year = {2022}, month = aug, doi = {10.4230/LIPIcs.FSCD.2022.5}, eprint = {2204.09421}, eprintclass = {cs.PL}, eprinttype = {arXiv}, isbn = {978-3-95977-233-4}, issn = {1868-8969}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Sheaf semantics of termination-insensitive noninterference}, volume = {228}, } In the published version of this paper, there were a few mistakes that have been corrected in the local copy hosted here. In the Critique of relational semantics for information flow, our discussion of the Failure of monotonicity stated incorrectly that algebras for the sealing monad at a higher security level could not be transformed into algebras for the sealing monad at a lower security level in the semantics of Abadi et al. This is not true, as pointed out to us privately by Carlos Tomé Cortiñas. What we meant to say was that it is not the case that a type whose component at a high security level is trivial shall always remain trivial at a lower security level. The original version of the extended edition of this paper, we claimed that the constructive existence of tensor products on pointed dcpos was obvious; in fact, tensor products do exist, but their construction involves a reflexive coequalizer of pointed dcpos.
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: 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. In Remark 5.15, we used the notation for the closed immersion prior to introducing it. We have fixed a few broken links in the bibliography. The local copy linked here has the corrections implemented.