Isabelleの文書
ここにまとめることにする。追加情報は追記していく。
配布に付いているPDF文書、同梱文書と呼ぶことにする。略称はファイルのベース名。
| タイトル | ページ数 | 略称 |
|---|---|---|
| Programming and Proving in Isabelle/HOL | 63 | prog-prove |
| A Proof Assistant for Higher-Order Logic | 223 | tutorial |
| Tutorial to Locales and Locale Interpretation | 20 | locales |
| Haskell-style type classes with Isabelle/Isar | 22 | classes |
| Defining (Co)datatypes and ... | 61 | datatype |
| Defining Recursive Functions in Isabelle/HOL | 20 | functions |
| Code generation from Isabelle/HOL theories | 43 | codegen |
| Picking Nits | 53 | nitpick |
| Hammering Away | 27 | sledgehummer |
| The Eisbach User Manual | 26 | eisbanch |
| LaTex Sugar for Isabelle Documents | 11 | suger |
| What’s in Main | 11 | main |
| The Isabelle/Isar Reference Manual | 341 | isar-ref |
| The Isabelle/Isar Implementation | 159 | implementation |
| The Isabelle System Manual | 40 | system |
| Isabelle/jEdit | 60 | jedit |
| Old Introduction to Isabelle | 77 | intro |
| Isabelle's Logics | 99 | logics |
| Isabelle’s Logics: FOL and ZF | 85 | logics-ZF |
| jEdit 5.3 User's Guide | 147 | jedit-manual |
| Haskebelle | 12 | haskebelle |
Isabelle/jEditでは、PDF文書が 11, 5, 3, 1, 1 のグループ分けしてあって、総計21文書。
ページ数だけ：
- 63
- 223
- 20
- 22
- 61
- 20
- 43
- 53
- 27
- 26
- 11
- 11
- 341
- 159
- 40
- 60
- 77
- 99
- 85
- 147
- 12
総計：1600ページ（ちょうど）
インターネット上の論文など
| タイトル | ベージ数 | 略称（リンク） | ローカル名 |
|---|---|---|---|
| A Tutorial Introduction to Structured Isar Proofs | 21 | isar-overview | isar-overview.pdf |
| Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit | 38 | 2010slide | |
| Isabelle/PIDE as Platform for Educational Tools | 11 | 2013edu | |
| PIDE as front-end technology of Coq | 13 | CoqPIDE | |
| Getting Started with Isabelle/jEdit | 6 | GetStart | Isabelle-PIDE_1208.1368.pdf |
| System description: Isabelle/jEdit in 2014 | 11 | SysDesc2014 | |
| Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit | 15 | Isabelle/Scala | |
| Isabelle/Isar ― a generic framework for human-readable proof documents | 20 | isar-framework | |
| Introduction to Interactive Theorem Proving with Isabelle/HOL | slide 27 | intro-slide | Isabelle-Isar_notes-2015-06-17.pdf |
| Isabelle Tutorial and User’s Manual | 144 | 1990-manual | 1990-IsabelleManual_UCAM-CL-TR-189.pdf |
| The Foundation of a Generic Theorem Prover | 37 | foundation | |
| Isabelle: The Next 700 Theorem Provers | 24 | next700 |
- 次の3つは同じだった。isar-overviewだ。
- isar-overviewは最新ではない。
- 2010slideとIsabelle/Scalaは話題は同じ Beyond Proof General で、どちらも2010
- isar-frameworkは、同梱isar-refのchapter 2 とほとんど同じ。
- 1990-manualの"5 Defining Logics"が参考になりそう。
- intro-slideは割と新しい（June 17th, 2015）
