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
To appear Sheaf semantics of termination-insensitive noninterference
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
To appear A stratified approach to Löb induction
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
To appear Normalization for multimodal type theory
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
A cost-aware logical framework
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
Normalization for Cubical Type theory
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
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
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
Preprint Crisp induction for intensional identity types
@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
Coming soon Synthetic Tait Computability for Simplicial Type Theory
J. Weinberger, B. Ahrens, U. Buchholtz, and P. North
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
Invited Normalization for initial space-valued models of type theories
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
Invited Naïve logical relations in synthetic Tait computability
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
A metalanguage for multi-phase modularity
@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
@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
@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},
}