Bibliography of Synthetic Tait Computability
Table of contents
This page collects all papers and dissertations about Synthetic Tait Computability / STC; 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, 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) April 19, 2022 @inproceedings{sterling-harper:2022, author = {Sterling, Jonathan and Harper, Robert}, editor = {Felty, Amy}, 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.15}, eprint = {2204.09421}, eprintclass = {cs.PL}, eprinttype = {arXiv}, number = {15}, 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 @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.3}, 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 @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 @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 @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 @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
2021 | @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
TYPES'22 | 28th International Conference on Types for Proofs and Programs June 2022 @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}, } |
WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 21, 2022 @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 @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}, } |
ML '21 | @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}, } |
Dissertations
Apr. 2022 | Dissertation Overview, Carnegie Mellon University @unpublished{sterling:2022:thesis:overview, author = {Sterling, Jonathan}, url = {https://www.jonmsterling.com/papers/sterling:2022:thesis:overview.pdf}, 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 @phdthesis{sterling:2021:thesis, author = {Sterling, Jonathan}, school = {Carnegie Mellon University}, year = {2021}, doi = {10.5281/zenodo.5709838}, note = {CMU technical report CMU-CS-21-142}, title = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory}, } |