| Implementing a modal dependent type theory D Gratzer, J Sterling, L Birkedal Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019 | 62 | 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 | 52 | 2021 |
| First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory J Sterling Carnegie Mellon University, 2022 | 44 | 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 | 39 | 2021 |
| Cubical Syntax for Reflection-Free Extensional Equality J Sterling, C Angiuli, D Gratzer | 29 | 2019 |
| 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 | 24 | 2022 |
| Algebraic Type Theory and Universe Hierarchies J Sterling | 21 | 2019 |
| Strict universes for Grothendieck topoi D Gratzer, M Shulman, J Sterling arXiv preprint arXiv:2202.12012, 2022 | 20* | 2022 |
| A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18, 2022 | 17 | 2022 |
| Syntactic categories for dependent type theory: sketching and adequacy D Gratzer, J Sterling arXiv preprint arXiv:2012.10783, 2020 | 17 | 2020 |
| Sheaf semantics of termination-insensitive noninterference J Sterling, R Harper FSCD 2022, 2022 | 16 | 2022 |
| Guarded computational type theory J Sterling, R Harper Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 15 | 2018 |
| Normalization by gluing for free λ-theories J Sterling, B Spitters arXiv preprint arXiv:1809.08646, 2018 | 12* | 2018 |
| Normalization-by-evaluation for modal dependent type theory D Gratzer, J Sterling, L Birkedal Technical report. July 2019. url: http://www. jonmsterling. com/pdfs/modal …, 2019 | 9 | 2019 |
| The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling arXiv preprint arXiv:1807.01869, 2018 | 9 | 2018 |
| Denotational semantics of general store and polymorphism J Sterling, D Gratzer, L Birkedal arXiv preprint arXiv:2210.02169, 2022 | 8 | 2022 |
| Higher order functions and Brouwer’s thesis J Sterling Journal of Functional Programming 31, e11, 2021 | 8* | 2021 |
| Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |
| Classifying topoi in synthetic guarded domain theory D Palombi, J Sterling Electronic Notes in Theoretical Informatics and Computer Science 1, 2023 | 5 | 2023 |
| 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 | 4 | 2024 |
Daniel GratzerAarhus UniversityVerified email at cs.au.dk
