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},
} |