Bibliography of Synthetic Tait Computability

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
Sheaf semantics of termination-insensitive noninterference
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
A stratified approach to Löb induction
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
Normalization for multimodal type theory
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
A cost-aware logical framework
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
Normalization for Cubical Type theory
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
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
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

Sep. 2022
Preprint Denotational semantics of general store and polymorphism
September 9, 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},
}
Jun. 2022
Preprint Naïve logical relations in synthetic Tait computability
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
Preprint Crisp induction for intensional identity types
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
Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
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
Invited Internal languages of diagrams of ∞-toposes
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
Invited Sheaf semantics of termination-insensitive noninterference
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
Synthetic Tait Computability for Simplicial Type Theory
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
Invited Normalization for initial space-valued models of type theories
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
Invited Naïve logical relations in synthetic Tait computability
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
Normalization for (Cartesian) Cubical Type Theory
MURI Team Meeting 2021
October 15, 2021
CT2021
Normalization for cubical type theory
ML '21
A metalanguage for multi-phase modularity
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},
}

Dissertations

Apr. 2022
Dissertation Overview: First Steps in Synthetic Tait Computability
Dissertation Overview, Carnegie Mellon University
BibTeX citation
@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
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
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
Invited Naïve logical relations in synthetic Tait computability
Proofs, Programs and Systems seminar (IRIF PPS)
June 9, 2022
Apr. 2022
Invited Intrinsic semantics of termination-insensitive noninterference
Boston University POPV Seminar
April 26, 2022
Dec. 2021
Invited Phase Distinctions in Type Theory
Topos Institute Colloquium
December 9, 2021
Nov. 2021
Invited Towards a geometry for syntax
Computer Laboratory, University of Cambridge
November 19, 2021
Nov. 2021
Between abstraction and composition...
Logic and Semantics Seminar, Aarhus University
November 1, 2021
Aug. 2021
Abstraction, composition, and the phase distinction
CMU Speakers Club
August 24, 2021
May 2021
Invited Normalization for Cubical Type Theory
Padova Logic Seminar
Apr. 2021
Invited Logical Relations As Types
CCS Colloquium, Augusta University
Feb. 2021
Normalization for Cubical Type theory
Pittsburgh's HoTT Seminar