‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language
Sebastian Ullrich, Leonardo de Moura
ICFP 2022 | August 2022
Lean
Programming language and theorem prover
Publications
Publications by Year
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
2022 International Joint Conference on Automated Reasoning | April 2022
-
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura, Sebastian Ullrich
2021 Conference on Automated Deduction | July 2021
-
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
IFL 2019 | March 2020
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
Developing Bug-Free Machine Learning Systems with Formal Mathematics
Daniel Selsam, Percy Liang, David L. Dill
ICML 2017 | July 2017
-
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
2016 International Joint Conference on Automated Reasoning | June 2016
-
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2015 Conference on Automated Deduction | July 2015
Publications by Research Area
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
2022 International Joint Conference on Automated Reasoning | April 2022
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura, Sebastian Ullrich
2021 Conference on Automated Deduction | July 2021
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
IFL 2019 | March 2020
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
Developing Bug-Free Machine Learning Systems with Formal Mathematics
Daniel Selsam, Percy Liang, David L. Dill
ICML 2017 | July 2017
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
2016 International Joint Conference on Automated Reasoning | June 2016
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2015 Conference on Automated Deduction | July 2015
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
2022 International Joint Conference on Automated Reasoning | April 2022
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura, Sebastian Ullrich
2021 Conference on Automated Deduction | July 2021
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
IFL 2019 | March 2020
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
Developing Bug-Free Machine Learning Systems with Formal Mathematics
Daniel Selsam, Percy Liang, David L. Dill
ICML 2017 | July 2017
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
2016 International Joint Conference on Automated Reasoning | June 2016
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2015 Conference on Automated Deduction | July 2015
-
‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language
Sebastian Ullrich, Leonardo de Moura
ICFP 2022 | August 2022
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
2022 International Joint Conference on Automated Reasoning | April 2022
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura, Sebastian Ullrich
2021 Conference on Automated Deduction | July 2021
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
IFL 2019 | March 2020
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
Developing Bug-Free Machine Learning Systems with Formal Mathematics
Daniel Selsam, Percy Liang, David L. Dill
ICML 2017 | July 2017
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
2016 International Joint Conference on Automated Reasoning | June 2016
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2015 Conference on Automated Deduction | July 2015
Publications by Type
-
‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language
Sebastian Ullrich, Leonardo de Moura
ICFP 2022 | August 2022
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
2022 International Joint Conference on Automated Reasoning | April 2022
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura, Sebastian Ullrich
2021 Conference on Automated Deduction | July 2021
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
IFL 2019 | March 2020
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
Developing Bug-Free Machine Learning Systems with Formal Mathematics
Daniel Selsam, Percy Liang, David L. Dill
ICML 2017 | July 2017
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
2016 International Joint Conference on Automated Reasoning | June 2016
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2015 Conference on Automated Deduction | July 2015