| Implementing a modal dependent type theory D Gratzer, J Sterling, L Birkedal Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019 | 74* | 2019 |
| Normalization for cubical type theory J Sterling, C Angiuli 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-15, 2021 | 62 | 2021 |
| First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory J Sterling Carnegie Mellon University, 2022 | 53 | 2022 |
| Logical relations as types: Proof-relevant parametricity for program modules J Sterling, R Harper Journal of the ACM (JACM) 68 (6), 1-47, 2021 | 44 | 2021 |
| A cost-aware logical framework Y Niu, J Sterling, H Grodin, R Harper Proceedings of the ACM on Programming Languages 6 (POPL), 1-31, 2022 | 35 | 2022 |
| Cubical Syntax for Reflection-Free Extensional Equality J Sterling, C Angiuli, D Gratzer | 32 | 2019 |
| Strict universes for Grothendieck topoi D Gratzer, M Shulman, J Sterling arXiv preprint arXiv:2202.12012, 2022 | 25* | 2022 |
| Algebraic Type Theory and Universe Hierarchies J Sterling | 23 | 2019 |
| A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18, 2022 | 20 | 2022 |
| Sheaf semantics of termination-insensitive noninterference J Sterling, R Harper FSCD 2022, 2022 | 20 | 2022 |
| Syntactic categories for dependent type theory: sketching and adequacy D Gratzer, J Sterling arXiv preprint arXiv:2012.10783, 2020 | 19 | 2020 |
| Guarded computational type theory J Sterling, R Harper Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 16 | 2018 |
| Normalization by gluing for free λ-theories J Sterling, B Spitters arXiv preprint arXiv:1809.08646, 2018 | 13* | 2018 |
| Denotational semantics of general store and polymorphism J Sterling, D Gratzer, L Birkedal arXiv preprint arXiv:2210.02169, 2022 | 10 | 2022 |
| Higher order functions and Brouwer’s thesis J Sterling Journal of Functional Programming 31, e11, 2021 | 10* | 2021 |
| The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling arXiv preprint arXiv:1807.01869, 2018 | 10 | 2018 |
| Decalf: A Directed, Effectful Cost-Aware Logical Framework H Grodin, Y Niu, J Sterling, R Harper Proceedings of the ACM on Programming Languages 8 (POPL), 273-301, 2024 | 7 | 2024 |
| The essence of generalized algebraic data types F Sieczkowski, S Stepanenko, J Sterling, L Birkedal Proceedings of the ACM on Programming Languages 8 (POPL), 695-723, 2024 | 6 | 2024 |
| Classifying topoi in synthetic guarded domain theory D Palombi, J Sterling Electronic Notes in Theoretical Informatics and Computer Science 1, 2023 | 6 | 2023 |
| Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |
Daniel GratzerAarhus UniversityVerified email at cs.au.dk