Lean (proof assistant)
Lean is a proof assistant and programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was principally developed by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history. Development is currently supported by the non-profit Lean Focused Research Organization (FRO).
| Paradigm | Functional programming, Imperative programming |
|---|---|
| Developer | Lean FRO |
| First appeared | 2013 |
| Stable release | 4.6.1
/ 4 March 2024 |
| Preview release | 4.7.0-rc2
/ 5 March 2024 |
| Typing discipline | Static, strong, inferred |
| Implementation language | Lean , C++ |
| OS | Cross-platform |
| License | Apache License 2.0 |
| Website | lean-lang |
| Influenced by | |
| ML Coq Haskell | |
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.