skip to content

Department of Computer Science and Technology

  • Associate Professor

Research

I study programming languages and semantics using type theory, category theory, domain theory, and topos theory as a guide.

Publications

Conference proceedings

  • Sterling, J., 2024 (Accepted for publication). Tensorial structure of the lifting doctrine in constructive domain theory
    Doi: 10.17863/CAM.108169
  • Sterling, J., Gratzer, D. and Birkedal, L., 2024. Towards Univalent Reference Types Leibniz International Proceedings in Informatics, LIPIcs, v. 288
    Doi: 10.4230/LIPIcs.CSL.2024.47
  • Aagaard, FL., Sterling, J. and Birkedal, L., 2023 (Accepted for publication). A denotationally-based program logic for higher-order store Proceedings of MFPS XXXIX,
    Doi: 10.46298/entics.12232
  • Sterling, J., 2023 (Accepted for publication). Towards univalent reference types
    Doi: 10.17863/CAM.105391
  • Sterling, J., 2023 (Accepted for publication). Towards a geometry for syntax
    Doi: 10.17863/CAM.106433
  • Sterling, J. and Harper, R., 2022. Sheaf Semantics of Termination-Insensitive Noninterference Leibniz International Proceedings in Informatics, LIPIcs, v. 228
    Doi: 10.4230/LIPIcs.FSCD.2022.5
  • Sterling, J. and Angiuli, C., 2021. Normalization for Cubical Type Theory Proceedings - Symposium on Logic in Computer Science, v. 2021-June
    Doi: 10.1109/LICS52264.2021.9470719
  • Sterling, J., Angiuli, C. and Gratzer, D., 2019. Cubical syntax for reflection-free extensional equality Leibniz International Proceedings in Informatics, LIPIcs, v. 131
    Doi: 10.4230/LIPIcs.FSCD.2019.31
  • Sterling, J. and Harper, R., 2018. Guarded computational type theory Proceedings - Symposium on Logic in Computer Science,
    Doi: 10.1145/3209108.3209153
  • Journal articles

  • Grodin, H., Niu, Y., Sterling, J. and Harper, R., 2024. Decalf: A Directed, Effectful Cost-Aware Logical Framework Proceedings of the ACM on Programming Languages, v. 8
    Doi: 10.1145/3632852
  • Sieczkowski, F., Stepanenko, S., Sterling, J. and Birkedal, L., 2024. The Essence of Generalized Algebraic Data Types Proceedings of the ACM on Programming Languages, v. 8
    Doi: 10.1145/3632866
  • Palombi, D. and Sterling, J., 2023 (Accepted for publication). Classifying topoi in synthetic guarded domain theory Electronic Notes in Theoretical Informatics and Computer Science, v. Volume 1 - Proceedings of...
    Doi: 10.46298/entics.10323
  • Sterling, J., 2023. What should a generic object be? Mathematical Structures in Computer Science, v. 33
    Doi: 10.1017/S0960129523000117
  • Sterling, J., Angiuli, C. and Gratzer, D., 2022. A CUBICAL LANGUAGE FOR BISHOP SETS Logical Methods in Computer Science, v. 18
    Doi: 10.46298/LMCS-18(1:43)2022
  • Niu, Y., Sterling, J., Grodin, H. and Harper, R., 2022. A cost-Aware logical framework Proceedings of the ACM on Programming Languages, v. 6
    Doi: 10.1145/3498670
  • Sterling, J. and Harper, R., 2021. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules Journal of the ACM, v. 68
    Doi: 10.1145/3474834
  • Sterling, J., 2021. Higher order functions and Brouwer’s thesis Journal of Functional Programming, v. 31
    Doi: 10.1017/S0956796821000095
  • Gratzer, D., Sterling, J. and Birkedal, L., 2019. Implementing a modal dependent type theory Proceedings of the ACM on Programming Languages, v. 3
    Doi: 10.1145/3341711
  • Angiuli, C., Cavallo, E., Favonia, KBH., Harper, R. and Sterling, J., 2018. The RedPRL proof assistant (invited paper) Electronic Proceedings in Theoretical Computer Science, EPTCS, v. 274
    Doi: 10.4204/EPTCS.274.1
  • Book chapters

  • McAdams, D. and Sterling, J., 2016. Dependent Types for Pragmatics
    Doi: 10.1007/978-3-319-26506-3_4
  • Contact Details

    Room: 
    FE24
    Email: 

    js2878@cam.ac.uk