Bibliography of Synthetic Tait Computability
Table of contents
This page collects all papers and dissertations about Synthetic Tait Computability / STC, also known as the logical relations as types / LRAT principle; if you have written a paper or dissertation involving STC, please write to me to have it added to this list.
The following authors are represented in this bibliography: Benedikt Ahrens, Carlo Angiuli, Lars Birkedal, Ulrik Buchholtz, Thierry Coquand, Daniel Gratzer, Harrison Grodin, Robert Harper, Yue Niu, Paige North, Jonathan Sterling, Taichi Uemura, and Jonathan Weinberger.
Refereed Publications
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}, } |
FSCD '22 | International Conference on Formal Structures for Computation and Deduction (FSCD) April 2022 BibTeX citation@inproceedings{gratzer-birkedal:2022, author = {Gratzer, Daniel and Birkedal, Lars}, editor = {Felty, Amy}, address = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, url = {https://jozefg.github.io/papers/a-stratified-approach-to-lob-induction.pdf}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, year = {2022}, month = aug, doi = {10.4230/LIPIcs.FSCD.2022.23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {A Stratified Approach to {L\"{o}b} Induction}, volume = {228}, } |
LICS '22 | Symposium on Logic and Computer Science (LICS) April 2022 BibTeX citation@inproceedings{gratzer:2022, title = {Normalization for Multimodal Type Theory}, author = {Gratzer, Daniel}, address = {New York, NY, USA}, publisher = {Association for Computing Machinery}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, year = {2022}, doi = {10.1145/3531130.3532398}, url = {https://jozefg.github.io/papers/2022-normalization-for-multimodal-type-theory-short.pdf}, } |
POPL '22 | 49th ACM SIGPLAN Symposium on Principles of Programming Languages January 2022 BibTeX citation@article{niu-sterling-grodin-harper:2022, author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert}, address = {New York, NY, USA}, publisher = {Association for Computing Machinery}, year = {2022}, month = jan, doi = {10.1145/3498670}, eprint = {2107.04663}, eprintclass = {cs.PL}, eprinttype = {arXiv}, journal = {Proceedings of the ACM on Programming Languages}, number = {POPL}, title = {A Cost-Aware Logical Framework}, volume = {6}, } |
LICS '21 | 36th Annual Symposium on Logic in Computer Science July 7, 2021 BibTeX citation@inproceedings{sterling-angiuli:2021, author = {Sterling, Jonathan and Angiuli, Carlo}, address = {Los Alamitos, CA, USA}, publisher = {IEEE Computer Society}, booktitle = {2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, year = {2021}, month = jul, doi = {10.1109/LICS52264.2021.9470719}, eprint = {2101.11479}, eprintclass = {cs.LO}, eprinttype = {arXiv}, pages = {1--15}, title = {Normalization for Cubical Type Theory}, } |
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}, } |
Unpublished Manuscripts
Dec. 2023 | December 22, 2023 BibTeX citation@unpublished{uemura:2022:coh, doi = {10.48550/ARXIV.2212.11764}, author = {Uemura, Taichi}, title = {Normalization and coherence for $\infty$-type theories}, publisher = {arXiv}, year = {2022}, } |
Dec. 2023 | December 5, 2023 BibTeX citation@unpublished{uemura:2022:diagrams, doi = {10.48550/ARXIV.2212.02444}, author = {Uemura, Taichi}, title = {Homotopy type theory as internal languages of diagrams of $\infty$-logoses}, publisher = {arXiv}, year = {2022}, } |
Oct. 2022 | Under review October 10, 2022 BibTeX citation@unpublished{gratzer-sterling-angiuli-coquand-birkedal:2022, doi = {10.48550/ARXIV.2210.05420}, author = {Gratzer, Daniel and Sterling, Jonathan and Angiuli, Carlo and Coquand, Thierry and Birkedal, Lars}, title = {Controlling unfolding in type theory}, year = {2022}, note = {Unpublished manuscript} } |
Oct. 2022 | Under review October 6, 2022 BibTeX citation@unpublished{sterling-gratzer-birkedal:2022, author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars}, year = {2022}, month = jul, note = {Unpublished manuscript}, title = {Denotational semantics of general store and polymorphism}, } |
Sep. 2022 | September 26, 2022 BibTeX citation@article{niu-harper:2022, doi = {10.48550/ARXIV.2209.12669}, author = {Niu, Yue and Harper, Robert}, title = {A metalanguage for cost-aware denotational semantics}, publisher = {arXiv}, year = {2022}, } |
Jun. 2022 | BibTeX citation@unpublished{sterling:2022:naive, author = {Sterling, Jonathan}, year = {2022}, month = jun, note = {Unpublished manuscript}, title = {Na\"{i}ve logical relations in synthetic {Tait} computability}, } |
2021 | BibTeX citation@unpublished{gratzer:2021:crisp-induction, author = {Gratzer, Daniel}, url = {https://jozefg.github.io/papers/crisp-induction-for-intensional-identity-types.pdf}, year = {2021}, note = {Unpublished manuscript}, title = {Crisp induction for intensional identity types}, } |
Workshop Presentations
HoTT/UF 22 | Workshop on Homotopy Type Theory / Univalent Foundations July 2022 BibTeX citation@misc{weinberger-ahrens-buchholtz-north:2022:hott-uf, author = {Weinberger, Jonathan and Ahrens, Benedikt and Buchholtz, Ulrik and North, Paige}, year = {2022}, month = july, note = {Workshop on Homotopy Type Theory / Univalent Foundations}, title = {Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability}, url = {https://hott-uf.github.io/2022/HoTTUF_2022_paper_6.pdf} } |
HoTT/UF 22 | Workshop on Homotopy Type Theory / Univalent Foundations July 2022 BibTeX citation@misc{uemura:2022:hott-uf, author = {Uemura, Taichi}, year = {2022}, month = july, note = {Workshop on Homotopy Type Theory / Univalent Foundations}, title = {Internal languages of diagrams of $\infty$-toposes}, url = {https://hott-uf.github.io/2022/uemura-hott-uf-2022-notes.pdf} } |
MURI '22 | MURI Team Meeting 2022 June 30, 2022 BibTeX citation@misc{sterling-harper:2022:muri, author = {Sterling, Jonathan and Harper, Robert}, url = {https://www.jonmsterling.com/slides/sterling:2022:muri.pdf}, year = {2022}, month = jun, note = {Talk given at the 2022 MURI Team Meeting}, title = {Sheaf semantics of termination-insensitive noninterference}, } |
TYPES '22 | 28th International Conference on Types for Proofs and Programs June 2022 BibTeX citation@inproceedings{weinberger-ahrens-buchholtz-north:2022:types, author = {Weinberger, Jonathan and Ahrens, Benedikt and Buchholtz, Ulrik and North, Paige}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, year = {2022}, title = {Synthetic {Tait} Computability for Simplicial Type Theory}, url = {https://types22.inria.fr/files/2022/06/TYPES_2022_paper_17.pdf} } |
WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 21, 2022 BibTeX citation@misc{uemura:2022:wg6, author = {Uemura, Taichi}, year = {2022}, month = may, note = {WG6 kick-off meeting: Syntax and Semantics of Type Theories}, title = {Normalization for initial space-valued models of type theories}, } |
WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 20, 2022 BibTeX citation@misc{sterling:2022:wg6, author = {Sterling, Jonathan}, year = {2022}, month = may, note = {WG6 kick-off meeting: Syntax and Semantics of Type Theories (Invited Talk)}, title = {Na\"{i}ve logical relations in synthetic {Tait} computability}, } |
MURI '21 | MURI Team Meeting 2021 October 15, 2021 |
ML '21 | BibTeX citation@unpublished{sterling-harper:2021:mlw, author = {Sterling, Jonathan and Harper, Robert}, url = {https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/5/A-metalanguage-for-multi-phase-modularity}, year = {2021}, month = aug, note = {ML 2021 abstract and talk}, title = {A metalanguage for multi-phase modularity}, } |
CT20→21 |
Dissertations
Apr. 2022 | Dissertation Overview, Carnegie Mellon University BibTeX citation@online{sterling:2022:thesis:overview, author = {Sterling, Jonathan}, url = {https://www.jonmsterling.com/forest/trees/jms-000q/}, year = {2022}, month = apr, note = {Synopsis of doctoral dissertation, Carnegie Mellon University}, title = {Dissertation Overview: \emph{First Steps in Synthetic {Tait} Computability}}, } |
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}, } |
Seminar Talks
Jun. 2022 | Proofs, Programs and Systems seminar (IRIF PPS) June 9, 2022 |
Apr. 2022 | Boston University POPV Seminar April 26, 2022 |
Dec. 2021 | Topos Institute Colloquium December 9, 2021 |
Nov. 2021 | Computer Laboratory, University of Cambridge November 19, 2021 |
Nov. 2021 | Logic and Semantics Seminar, Aarhus University November 1, 2021 |
Aug. 2021 | CMU Speakers Club August 24, 2021 |
May 2021 | Padova Logic Seminar |
Apr. 2021 | CCS Colloquium, Augusta University |
Feb. 2021 | Pittsburgh's HoTT Seminar |