stella

stella は MoonBit で書かれた、現在開発中の証明支援系です。そのカーネルは elab パッケージで、Martin-Löf 型理論のコア構文、値への評価、正規形への読み戻し、そして評価による正規化で定義的等価性を判定する双方向型検査器を提供します。

この型理論は、ユニット型、 $\Pi$ 型、 $\Sigma$ 型、 $J$ 除去子を伴う同一性型、再帰を伴う W 型、可述的宇宙の累積的階層を持ち、 $\Pi$ 型の定義域について反変な部分型付けを備えています。

パッケージ

パッケージ	内容	API	チュートリアル	設計
`elab` (`src/elab`)	項（`TermInf`、`TermChk`、`Name`）、値（`Value`、`Neutral`）、評価と読み戻し（`eval_inf`、`eval_chk`、`quote`）、型検査（`type_inf`、`type_chk`、`type_inf_0`、`def_eq`、`TypeError`）。	API	チュートリアル	設計

このパッケージには、宇宙レベル、部分型付け、注釈の型付けに関するホワイトボックステスト（elaboration_wbtest.mbt）も含まれています。

依存型が初めての方。 下の論考を $\lambda\Pi$ 計算の章まで読み、それからチュートリアルに取り組んでください。恒等関数、ペア、パス帰納法による証明を MoonBit の値として構築します。
カーネルを使う方。 チュートリアルでは定数の宣言、項の検査と正規化の方法を示し、API リファレンスでは、いつ TypeError を送出し、いつ panic するかを含め、各関数の契約を述べています。
カーネルを開発する方。 設計ノートでは、すべての型付け規則を推論規則の記法で示し、評価と読み戻しの等式、検査器が依存する不変条件、実装と理論の間の既知の欠落を述べています。

stella には moonc 0.10 以降の MoonBit が必要で、MoonBit コアライブラリ以外の依存関係はありません。

moon add Luna-Flow/stella@0.1.2

import {
  "Luna-Flow/stella/elab",
  "moonbitlang/core/list",
}

プルリクエストを出す前に moon check --target all と moon test を実行してください。

以下の論考は、型なしラムダ計算から Martin-Löf 型理論までを順に展開して stella の背後にある型理論を説明し、カーネルがそれをどのようにエラボレートするかを解説します。エラボレーションの詳細に取り組んだり証明言語を拡張したりする前に、全体像をつかむための概説として読んでください。