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 |