nLab Jonathan Sterling (changes)

Showing changes from revision #15 to #16: Added | Removed | Changed

• personal page

• institute page

• MathGenealogy page

• GoogleScholar page

Selected writings

See also the personal bibliography.

\linebreak

On synthetic domain theory:

• Jonathan Sterling, Lingyuan Ye, Domains and Classifying Topoi (arXiv:2505.13096)

• Leoni Pugh, Jonathan Sterling, When is the partial map classifier a Sierpiński cone? (arXiv:2504.06789)

On guarded recursion:

• Jonathan Sterling ,

  Jonathan Sterling, Robert Harper, Guarded Computational Type Theory, LICS ‘18 (2018) 879–888 [[arxiv:1804.09098](https://arxiv.org/abs/1804.09098), doi:10.1145/3209108.3209153]

  Robert Harper , Guarded Computational Type Theory, LICS ‘18 (2018) 879–888 [[arxiv:1804.09098](https://arxiv.org/abs/1804.09098), doi:10.1145/3209108.3209153]

• Daniele Palombi, Jonathan Sterling, Classifying topoi in synthetic guarded domain theory, Proceedings of MFPS XXXVIII (2023) [[arxiv:2210.04636](https://arxiv.org/abs/2210.04636)],[[doi:10.46298/entics.10323](https://doi.org/10.46298/entics.10323)]

On categorical models of dependent types via locally Cartesian closed categories:

• Daniel Gratzer, Jonathan Sterling, Syntactic categories for dependent type theory: sketching and adequacy [[arXiv:2012.10783](https://arxiv.org/abs/2012.10783)]

On synthetic Tait computability theory:

• Jonathan Sterling, First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory (2021) [[PhD thesis](https://www.jonmsterling.com/sterling-2021-thesis/)]

• Jonathan Sterling, Naïve logical relations in synthetic Tait computability (2022) [[pdf](https://www.jonmsterling.com/bafkrmialyvkzh6w6snnzr3k4h2b62bztsk4le57idughqik24bltinieki.pdf)]

On XTT:

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).

On synthetic domain theory via classifying topos theory:

• Jonathan Sterling, Lingyuan Ye: Domains and Classifying Topoi [[arXiv:2505.13096](https://arxiv.org/abs/2505.13096)]

Related entries

• meaning explanation

• cubical type theory

• XTT