skip to content
Home

Department of Computer Science and Technology

Faculty Subscribe to RSS - Faculty

Singular: 
Faculty
Slug: 
faculty
Read more at: Dr Prakash Murali

Dr Prakash Murali

My research interests include quantum architecture, resource estimation and compilation. I was previously a Senior Quantum Systems Architect as part of Microsoft's quantum computing program where I designed the Azure Quantum Resource Estimator to understand the resource needs of practical-scale quantum applications. I graduated with a Computer Science Ph.D. from Princeton University.

Read more at: Dr Rika Antonova

Dr Rika Antonova

A Brief Bio

Read more at: Dr Tobias Grosser

Dr Tobias Grosser

My interests are compilation, programming language design, and effective performance programming. However, I define these areas broadly. As a result, I ask questions such as:

Read more at: Dr Fermin Moscoso del Prado Martin

Dr Fermin Moscoso del Prado Martin

Read more at: Dr Jon Sterling

Dr Jon Sterling

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
    •
  • 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
    •
  • 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. 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
    •
  • 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., 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
    •
  • Sterling, J., 2021. Higher order functions and Brouwer’s thesis Journal of Functional Programming, v. 31
    Doi: 10.1017/S0956796821000095
    •
  • 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
    •
  • 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
    •
    Conference proceedings

    2024 (Accepted for publication)

  • Sterling, J., 2024 (Accepted for publication). Tensorial structure of the lifting doctrine in constructive domain theory
    Doi: 10.17863/CAM.108169
    •

    2024

  • 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
    •

    2023 (Accepted for publication)

  • 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
    •

    2022

  • 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
    •

    2021

  • 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
    •

    2019

  • 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
    •

    2018

  • Sterling, J. and Harper, R., 2018. Guarded computational type theory Proceedings - Symposium on Logic in Computer Science,
    Doi: 10.1145/3209108.3209153
    •
    Journal articles

    2024

  • 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
    •

    2023 (Accepted for publication)

  • 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
    •

    2023

  • Sterling, J., 2023. What should a generic object be? Mathematical Structures in Computer Science, v. 33
    Doi: 10.1017/S0960129523000117
    •

    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., 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
    •

    2021

  • Sterling, J., 2021. Higher order functions and Brouwer’s thesis Journal of Functional Programming, v. 31
    Doi: 10.1017/S0956796821000095
    •
  • 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
    •

    2019

  • 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
    •

    2018

  • 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

    2016

  • McAdams, D. and Sterling, J., 2016. Dependent Types for Pragmatics
    Doi: 10.1007/978-3-319-26506-3_4
    •
    Jem Lord
    Lingyuan Ye
    Andrew Slattery
    Read more at: Prof. Tom Gur

    Prof. Tom Gur

    About Me

    I am a Professor in the Department of Computer Science and Technology at the University of Cambridge.

    Read more at: Dr Weiwei Sun

    Dr Weiwei Sun

    Read more at: Dr Carl Henrik Ek

    Dr Carl Henrik Ek

    You can find my personal home page here.

    Read more at: Nic Lane

    Nic Lane

    Please visit my personal website (http://niclane.org) or my lab website (http://mlsys.cst.cam.ac.uk/) for the most up-to-date and complete information (including papers).

    Read more at: Ferenc Huszár

    Ferenc Huszár

    I'm interested in the principles of machine learning, with a particular focus on modern deep learning methods. My research falls into the following themes:

    Department of Computer Science and Technology
    University of Cambridge
    William Gates Building
    15 JJ Thomson Avenue
    Cambridge
    CB3 0FD

    About the department

    Study here
    Research
    News
    Jobs
    How to get here
    About the department

    Contact us

    Website privacy policy

    Social media

    Athena Swan bronze award logo

    Study at Cambridge

    About the University

    Research at Cambridge