Lean: Past, Present, and Future (Invited Talk)
Published in 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, 2024
Publications
'do' unchained: embracing local imperativity in a purely functional language (functional pearl)
Published in Proc. ACM Program. Lang., 2022
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Published in Log. Methods Comput. Sci., 2022
The Lean 4 Theorem Prover and Programming Language
Published in Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, 2021
Counting immutable beans: reference counting optimized for purely functional programming
Published in IFL '19: Implementation and Application of Functional Languages, Singapore, September 25-27, 2019, 2019
A metaprogramming framework for formal verification
Published in Proc. ACM Program. Lang., 2017
Verified construction of static single assignment form
Published in Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, 2016