| A Metaprogramming Framework for Formal Verification G Ebner, S Ullrich, J Roesch, J Avigad, L de Moura Proceedings of the ACM on Programming Languages 1 (ICFP), 34, 2017 | 91 | 2017 |
| The Lean 4 Theorem Prover and Programming Language (System Description) L de Moura, S Ullrich Proceedings of the 28th International Conference on Automated Deduction, 2021 | 59* | 2021 |
| Simple Verification of Rust Programs via Functional Purification S Ullrich Karlsruhe Institute of Technology, 2016 | 19 | 2016 |
| Counting immutable beans: Reference counting optimized for purely functional programming S Ullrich, L de Moura Proceedings of the 31st Symposium on Implementation and Application of …, 2019 | 18 | 2019 |
| Verified construction of static single assignment form S Buchwald, D Lohner, S Ullrich Proceedings of the 25th International Conference on Compiler Construction, 67-76, 2016 | 13 | 2016 |
| Beyond notations: Hygienic macro expansion for theorem proving languages S Ullrich, L de Moura International Joint Conference on Automated Reasoning, 167-182, 2020 | 12 | 2020 |
| Tabled typeclass resolution D Selsam, S Ullrich, L de Moura arXiv preprint arXiv:2001.04301, 2020 | 10 | 2020 |
| Verified Construction of Static Single Assignment Form S Ullrich, D Lohner Archive of Formal Proofs, 2016 | 3 | 2016 |
| The Lean reference manual J Avigad, G Ebner, S Ullrich | 2 | 2017 |
| Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages L de Moura, S Ullrich Logical Methods in Computer Science 18, 2022 | | 2022 |
| ‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl) S Ullrich, L de Moura Proceedings of the ACM on Programming Languages 6 (ICFP), 512–539, 2022 | | 2022 |
Leonardo de MouraSenior Principal Researcher at MicrosoftVerified email at microsoft.com
