Verified construction of static single assignment form. - Sebastian Buchwald; Denis Lohner; Sebastian Ullrich 002 (CC, 2016)

Verified Construction of Static Single Assignment Form. - Sebastian Ullrich 002; Denis Lohner (Arch. Formal Proofs, 2016)

A metaprogramming framework for formal verification. - Gabriel Ebner; Sebastian Ullrich 002; Jared Roesch; Jeremy Avigad; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2017)

Counting immutable beans: reference counting optimized for purely functional programming. - Sebastian Ullrich 002; Leonardo de Moura 001 (IFL, 2019)

Tabled Typeclass Resolution. - Daniel Selsam; Sebastian Ullrich 002; Leonardo de Moura 001 (CoRR, 2020)

The Lean 4 Theorem Prover and Programming Language. - Leonardo de Moura 001; Sebastian Ullrich 002 (CADE, 2021)

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. - Sebastian Ullrich 002; Leonardo de Moura 001 (Log. Methods Comput. Sci., 2022)

'do' unchained: embracing local imperativity in a purely functional language (functional pearl). - Sebastian Ullrich 002; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2022)

An Extensible Theorem Proving Frontend. - Sebastian Ullrich 002 (2023)

Lean: Past, Present, and Future (Invited Talk). - Sebastian Ullrich 002 (FSCD, 2024)