Lean (証明アシスタント)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/05/26 13:31 UTC 版)
Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)でもある。帰納型を伴うCalculus of constructionsと呼ばれる型システムに基づいている。純粋関数型言語であるが、functional but in-place と呼ばれるプログラミングパラダイムに基づいており、効率性を重視している。
- ^ “Lean Prover About Page”. 2023年7月7日閲覧。
- ^ Sebastian Ullrich (2023). An Extensible Theorem Proving Frontend. Karlsruhe Institute of Technology. "1.3.3 The Essence of Lean"
- ^ a b c Sebastian Ulrich (2023). “An Extensible Theorem Proving Frontend”. Karlsruhe Institute of Technology. "1.3.4 A Short History of Lean"
- ^ “Releases/v3.0.0”. GitHub. 2024年4月27日閲覧。
- ^ “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ a b c Leonardo de Moura, Sebastian Ullrich (2021). “The Lean 4 Theorem Prover and Programming Language”. 28th International Conference on Automated Deduction (CADE-28).
- ^ “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。
- ^ “Mathlib porting status”. 2024年3月25日閲覧。
- ^ “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。
- ^ “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ a b “Tabled Typeclass Resolution”. arxiv. 2024年5月25日閲覧。
- ^ 型に応じて、同じ処理に複数の実装を提供すること
- ^ “An Abstract Machine for Tabled Execution of Fixed-Order Stratified Logic Programs”. ResearchGate. 2024年5月4日閲覧。
- ^ “‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)”. ACM. 2024年5月25日閲覧。
- ^ “What is the Xena project?”. Kevin Buzzard. 2024年4月27日閲覧。
- ^ “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。
- ^ “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。
- ^ “Lean Into Verified Software Development”. AWS. 2024年5月24日閲覧。
[続きの解説]
「Lean (証明アシスタント)」の続きの解説一覧
- 1 Lean (証明アシスタント)とは
- 2 Lean (証明アシスタント)の概要
- 3 Lean の特徴
- 4 利用
- Lean (証明アシスタント)のページへのリンク
