Errata
FSCD '22 | International Conference on Formal Structures for Computation and Deduction (FSCD) 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.
|
Sep. 2021 | Doctoral Dissertation, Carnegie Mellon University 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 | Journal of the ACM 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:
The local copy linked here has the corrections implemented. |