Leonardo de Moura

Karlsruhe Institute of Technology — Germany

Computer Science · Physical Sciences

40h-index13.4kcitations99works0.02yr avg
OpenAlex↗ORCID↗Google Scholar↗Lab page↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Formal Methods in Verification(63), Logic, programming, and type systems(61), Logic, Reasoning, and Knowledge(25), Software Testing and Debugging Techniques(20), Constraint Satisfaction and Optimization(10)

Publications99 total

‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)
Proceedings of the ACM on Programming Languages·2022· 5 citedOpen Access
Supplement of "'do' Unchained: Embracing Local Imperativity in a Purely Functional Language"
2022Open Access
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Logical Methods in Computer Science·2022· 5 citedOpen Access
Use and Abuse of Instance Parameters in the Lean Mathematical Library
DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)·2022· 7 citedOpen Access
Perceus: garbage free reference counting with reuse
2021· 27 citedOpen Access
The Lean 4 Theorem Prover and Programming Language
Lecture notes in computer science·2021· 149 citedOpen Access
Universal Policies for Software-Defined MDPs
arXiv (Cornell University)·2020· 1 citedOpen Access
Sealing pointer-based optimizations behind pure functions
Proceedings of the ACM on Programming Languages·2020Open Access
Preface: Selected Extended Papers of CADE 2017
Journal of Automated Reasoning·2020Open Access
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
arXiv (Cornell University)·2020Open Access
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge
arXiv (Cornell University)·2020· 11 citedOpen Access
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Lecture notes in computer science·2020· 10 citedOpen Access
Counting immutable beans
2019· 20 cited
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
arXiv (Cornell University)·2019· 3 citedOpen Access
Mimalloc: Free List Sharding in Action
Lecture notes in computer science·2019· 62 cited
Programming Z3
Lecture notes in computer science·2019· 37 cited
Learning a SAT Solver from Single-Bit Supervision
arXiv (Cornell University)·2018· 189 citedOpen Access
Applications and Challenges in Satisfiability Modulo Theories
EPiC series in computing·2018· 2 cited
Theorem Proving in Lean
Figshare·2018· 7 citedOpen Access
A metaprogramming framework for formal verification
Proceedings of the ACM on Programming Languages·2017· 79 citedOpen Access
page 1 of 5Next →

Frequent Co-authors

Nikolaj Bjørner(11), Dejan Jovanović(6), Harald Rueß(6), Bruno Dutertre(4), John Rushby(4), Clark Barrett(4), Natarajan Shankar(4), Jeremy Avigad(3), Maria Sorea(3), Sam Owre(3), Aaron Stump(3), Grégoire Hamon(3), Christoph M. Wintersteiger(3), Soonho Kong(2), María Inés de Frutos-Fernández(2), Jakob von Raumer(2), Sebastian Ullrich(2), Youssef Hamadi(2), Daan Leijen(2), Grant Olney Passmore(2)