テーゼ： 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…