Tauto プログラミング言語入門

コードを書き、その正しさを証明する言語 Tauto を、値と関数から所有権・代数的効果・依存型・定理証明まで 24 章で学ぶ入門書です。

1. Tauto という言語
2. 最初のプログラム
3. 値・変数・基本型
4. 関数と制御フロー
5. 構造体・列挙型・パターンマッチ
6. リスト・ジェネリクス・型クラス
7. 所有権の四つの種
8. 借用と参照
9. 代数的効果とは何か
10. 継続の回数と所有権
11. 実行の上限を設定する
12. プロジェクト・テスト・ツール
13. 証明の第一歩
14. 等式を証明する
15. 帰納法と再帰
16. タクティクと証明のステップ
17. 依存型と型の宇宙
18. 実例：ソートの正しさ
19. 実例：状態遷移と不変条件
20. 何が保証され、何が保証されないか
21. これから何を作るか
22. 付録A 構文早見表
23. 付録B 演習のヒントと解答
24. 付録C 用語集と学習チェックリスト