Leonardo de Moura

Publication Activity (10 Years)

Years Active: 2012-2021
Publications (10 Years): 19

Top Topics

Automated Deduction

Formal Verification

Functional Programming

Top Venues

Proc. ACM Program. Lang.

Publications

Leonardo de Moura, Sebastian Ullrich
The Lean 4 Theorem Prover and Programming Language. CADE (2021)
Alex Reinking, Ningning Xie, Leonardo de Moura, Daan Leijen
Perceus: garbage free reference counting with reuse. PLDI (2021)
Sebastian Ullrich, Leonardo de Moura
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. CoRR (2020)
Sebastian Ullrich, Leonardo de Moura
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. IJCAR (2) (2020)
Daniel Selsam, Simon Hudon, Leonardo de Moura
Sealing pointer-based optimizations behind pure functions. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Leonardo de Moura
Preface: Selected Extended Papers of CADE 2017. J. Autom. Reason. 64 (3) (2020)
Daniel Selsam, Jesse Michael Han, Leonardo de Moura, Patrice Godefroid
Universal Policies for Software-Defined MDPs. CoRR (2020)
Daniel Selsam, Sebastian Ullrich, Leonardo de Moura
Tabled Typeclass Resolution. CoRR (2020)
Daniel Selsam, Simon Hudon, Leonardo de Moura
Sealing Pointer-Based Optimizations Behind Pure Functions. CoRR (2020)
Sebastian Ullrich, Leonardo de Moura
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. CoRR (2019)
Daan Leijen, Benjamin Zorn, Leonardo de Moura
Mimalloc: Free List Sharding in Action. APLAS (2019)
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
Learning a SAT Solver from Single-Bit Supervision. ICLR (Poster) (2019)
Sebastian Ullrich, Leonardo de Moura
Counting immutable beans: reference counting optimized for purely functional programming. IFL (2019)
Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph M. Wintersteiger
Programming Z3. SETSS (2018)
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
Learning a SAT Solver from Single-Bit Supervision. CoRR (2018)
Daniel Selsam, Leonardo de Moura
Congruence Closure in Intensional Type Theory. CoRR (2017)
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Leonardo de Moura
Formalizing Mathematics using the Lean Theorem Prover. ISAIM (2016)
Daniel Selsam, Leonardo de Moura
Congruence Closure in Intensional Type Theory. IJCAR (2016)
Dejan Jovanovic, Leonardo de Moura
Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46 (3/4) (2012)