<commit_before>---
layout: archive
title: "Publications"
date:
modified:
excerpt:
image:
  feature:
  teaser:
  thumb:
ads: false
---

This is a list of papers and presentations about Lean by the Lean developers. For further publications about Lean, the mathlib library, and other formalizations in Lean, please also see [the Lean community website](https://leanprover-community.github.io/papers.html).

## Papers

- "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)" [PDF](/papers/do.pdf), [Supplement repository](https://github.com/Kha/do-supplement)<br />
  [<NAME>][kha], [<NAME>][leo],<br /> 27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022), Ljubljana, Slovenia, 2022.

- "The Lean 4 Theorem Prover and Programming Language" [PDF](/papers/lean4.pdf)<br />
  [<NAME>][leo], [<NAME>][kha],<br />28th International Conference on Automated Deduction (CADE-28), Pittsburgh, USA, 2021.

- "Tabled Typeclass Resolution" [PDF](https://arxiv.org/pdf/2001.04301.pdf)<br />
  [<NAME>][daniel], [<NAME>][kha], [<NAME>][leo], <br />
  draft, 2020. <br/>

- "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages" [PDF](https://arxiv.org/pdf/2001.10490.pdf)<br />
  [<NAME>][kha], [<NAME>][leo], <br />
  10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, 2020.

- "Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming." [PDF](https://arxiv.org/abs/1908.05647), [Appendix](/papers/beans_appendix.pdf) <br /> [<NAME>][kha], [<NAME>][leo],<br />
  The 31st symposium on Implementation and Application of Functional Languages (IFL 2019), Singapore, 2019.<br/>

- "A Metaprogramming Framework for Formal Verification." [PDF](/papers/tactic.pdf)<br />
  [<NAME>][gabriel], [<NAME>][kha], [<NAME>][jared], [<NAME>][jeremy], [<NAME>][leo],<br />22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017), Oxford, UK, 2017.

- ["Developing Bug-Free Machine Learning Systems With Formal Mathematics."](https://arxiv.org/abs/1706.08605) [Source code](https://github.com/dselsam/certigrad) <br />
  [<NAME>][daniel], <NAME>, <NAME>, Thirty-fourth International Conference on Machine Learning (ICML) 2017.<br />

- "Congruence Closure in Intensional Type Theory." [PDF](/papers/congr.pdf)<br />
  [<NAME>][daniel] and [<NAME>][leo], <br />
  International Joint Conference on Automated Reasoning (IJCAR), Coimbra, Portugal, 2016.

- "The Lean Theorem Prover." [PDF](/papers/system.pdf)<br />
  [<NAME>][leo], [<NAME>][soonho], [<NAME>][jeremy], [<NAME>][floris] and [<NAME>][jakob],<br />25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015.

- "Elaboration in Dependent Type Theory." [PDF][constr] <br />
  [<NAME>][leo], [<NAME>][jeremy], [<NAME>][soonho] and [<NAME>][cody]<br />
  A description of the elaborator used in Lean 2 only.

[leo]: http://leodemoura.github.io/
[soonho]: http://www.cs.cmu.edu/~soonhok
[jeremy]: http://www.andrew.cmu.edu/user/avigad
[floris]: http://www.contrib.andrew.cmu.edu/~fpv
[jakob]: http://von-raumer.de/
[cody]: http://www.andrew.cmu.edu/user/croux
[constr]: http://arxiv.org/abs/1505.04324
[gabriel]: https://gebner.org/
[kha]: https://pp.ipd.kit.edu/~ullrich/
[jared]: http://jroesch.github.io/
[daniel]: http://stanford.edu/~dselsam/

## Presentations

- [‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)](http://leanprover.github.io/talks/icfp2022.pdf) [[video]](https://youtu.be/nqBVYQh6Lxo), [ICFP 2022](https://icfp22.sigplan.org/), September 2022.

- [Lean 4](http://leanprover.github.io/talks/ICERM-2022.pdf), [Lean for the Curious Mathematician](https://icerm.brown.edu/topical_workshops/tw-22-lean/), [[video]](https://icerm.brown.edu/video_archive/?play=2906), July 2022.

- [An Introduction to the Lean 4 theorem prover and programming language](http://leanprover.github.io/talks/NFM2022.pdf), [NASA Formal Methods Symposium](https://nfm2022.caltech.edu/), May 2022.

- [Gotta Prove Fast: Building an Ecosystem for Eﬀortless Native Compilation of Tactics](http://leanprover.github.io/talks/WITS2022.pdf) [[video]](https://youtu.be/Tn74XMuTyM8), [Workshop on the Implementation of Type Systems 2022](https://popl22.sigplan.org/home/wits-2022), January 2022.

- Metaprogramming in Lean 4 [[slides pt. 1]](https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf) [[slides pt. 2]](https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf) [[video]](https://www.youtube.com/watch?v=hxQ1vvhYN_U) [[video cont.]](https://www.youtube.com/watch?v=vy4JWIiiXSY), [Lean Together 2021](https://leanprover-community.github.io/lt2021/), January 2021.<commit_msg>RacketCon 2022 slides<commit_after>---
layout: archive
title: "Publications"
date:
modified:
excerpt:
image:
  feature:
  teaser:
  thumb:
ads: false
---

This is a list of papers and presentations about Lean by the Lean developers. For further publications about Lean, the mathlib library, and other formalizations in Lean, please also see [the Lean community website](https://leanprover-community.github.io/papers.html).

## Papers

- "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)" [PDF](/papers/do.pdf), [Supplement repository](https://github.com/Kha/do-supplement)<br />
  [<NAME>][kha], [<NAME>][leo],<br /> 27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022), Ljubljana, Slovenia, 2022.

- "The Lean 4 Theorem Prover and Programming Language" [PDF](/papers/lean4.pdf)<br />
  [<NAME>][leo], [<NAME>][kha],<br />28th International Conference on Automated Deduction (CADE-28), Pittsburgh, USA, 2021.

- "Tabled Typeclass Resolution" [PDF](https://arxiv.org/pdf/2001.04301.pdf)<br />
  [<NAME>][daniel], [<NAME>][kha], [<NAME>][leo], <br />
  draft, 2020. <br/>

- "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages" [PDF](https://arxiv.org/pdf/2001.10490.pdf)<br />
  [<NAME>][kha], [<NAME>][leo], <br />
  10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, 2020.

- "Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming." [PDF](https://arxiv.org/abs/1908.05647), [Appendix](/papers/beans_appendix.pdf) <br /> [<NAME>][kha], [<NAME>][leo],<br />
  The 31st symposium on Implementation and Application of Functional Languages (IFL 2019), Singapore, 2019.<br/>

- "A Metaprogramming Framework for Formal Verification." [PDF](/papers/tactic.pdf)<br />
  [Gab<NAME>][gabriel], [<NAME>][kha], [<NAME>][jared], [<NAME>][jeremy], [<NAME>][leo],<br />22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017), Oxford, UK, 2017.

- ["Developing Bug-Free Machine Learning Systems With Formal Mathematics."](https://arxiv.org/abs/1706.08605) [Source code](https://github.com/dselsam/certigrad) <br />
  [<NAME>][daniel], <NAME>, <NAME>, Thirty-fourth International Conference on Machine Learning (ICML) 2017.<br />

- "Congruence Closure in Intensional Type Theory." [PDF](/papers/congr.pdf)<br />
  [<NAME>][daniel] and [<NAME>][leo], <br />
  International Joint Conference on Automated Reasoning (IJCAR), Coimbra, Portugal, 2016.

- "The Lean Theorem Prover." [PDF](/papers/system.pdf)<br />
  [<NAME>][leo], [<NAME>][soonho], [<NAME>][jeremy], [<NAME>][floris] and [<NAME>][jakob],<br />25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015.

- "Elaboration in Dependent Type Theory." [PDF][constr] <br />
  [<NAME>][leo], [<NAME>][jeremy], [So<NAME>][soonho] and [<NAME>][cody]<br />
  A description of the elaborator used in Lean 2 only.

[leo]: http://leodemoura.github.io/
[soonho]: http://www.cs.cmu.edu/~soonhok
[jeremy]: http://www.andrew.cmu.edu/user/avigad
[floris]: http://www.contrib.andrew.cmu.edu/~fpv
[jakob]: http://von-raumer.de/
[cody]: http://www.andrew.cmu.edu/user/croux
[constr]: http://arxiv.org/abs/1505.04324
[gabriel]: https://gebner.org/
[kha]: https://pp.ipd.kit.edu/~ullrich/
[jared]: http://jroesch.github.io/
[daniel]: http://stanford.edu/~dselsam/

## Presentations

- [Metaprograms and Proofs: Macros in Lean 4](http://leanprover.github.io/talks/RacketCon2022.pdf), [RacketCon 2022](https://con.racket-lang.org/), October 2022.

- [‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)](http://leanprover.github.io/talks/icfp2022.pdf) [[video]](https://youtu.be/nqBVYQh6Lxo), [ICFP 2022](https://icfp22.sigplan.org/), September 2022.

- [Lean 4](http://leanprover.github.io/talks/ICERM-2022.pdf), [Lean for the Curious Mathematician](https://icerm.brown.edu/topical_workshops/tw-22-lean/), [[video]](https://icerm.brown.edu/video_archive/?play=2906), July 2022.

- [An Introduction to the Lean 4 theorem prover and programming language](http://leanprover.github.io/talks/NFM2022.pdf), [NASA Formal Methods Symposium](https://nfm2022.caltech.edu/), May 2022.

- [Gotta Prove Fast: Building an Ecosystem for Eﬀortless Native Compilation of Tactics](http://leanprover.github.io/talks/WITS2022.pdf) [[video]](https://youtu.be/Tn74XMuTyM8), [Workshop on the Implementation of Type Systems 2022](https://popl22.sigplan.org/home/wits-2022), January 2022.

- Metaprogramming in Lean 4 [[slides pt. 1]](https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf) [[slides pt. 2]](https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf) [[video]](https://www.youtube.com/watch?v=hxQ1vvhYN_U) [[video cont.]](https://www.youtube.com/watch?v=vy4JWIiiXSY), [Lean Together 2021](https://leanprover-community.github.io/lt2021/), January 2021.
{'fraction_non_alphanumeric': 0.18010642652476463, 'fraction_numerical': 0.04471960704052395, 'mean_word_length': 5.150409062303336, 'pattern_counts': {'":': 0, '<': 107, '<?xml version=': 0, '>': 107, 'https://': 43, 'lorem ipsum': 0, 'www.': 12, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2319649', 'n_tokens_mistral': 3942, 'n_tokens_neox': 3461, 'n_words': 782}