unsoundsystem

<p>色々な定理証明支援系の機能･特徴などをまとめていきます｡あまり知らないので教えて頂けると嬉しいです｡</p>
<table>
<thead>
<tr>
<th style="text-align:center">名前</th>
<th style="text-align:center">依存型</th>
<th style="text-align:center">Extraction<sup class="footnote-ref"><a href="#fn-991d-1" id="fnref-991d-1">[1]</a></sup>
</th>
<th style="text-align:center">Link</th>
</tr>
</thead>
<tbody>
<tr>
<td style="text-align:center">Isabelle</td>
<td style="text-align:center"></td>
<td style="text-align:center">Haskell, OCaml, SML, Scala</td>
<td style="text-align:center"><a href="https://isabelle.in.tum.de" target="_blank" rel="nofollow noopener noreferrer">https://isabelle.in.tum.de</a></td>
</tr>
<tr>
<td style="text-align:center">Coq</td>
<td style="text-align:center">Yes</td>
<td style="text-align:center">Haskell, OCaml, Scheme</td>
<td style="text-align:center"><a href="https://coq.inria.fr" target="_blank" rel="nofollow noopener noreferrer">https://coq.inria.fr</a></td>
</tr>
<tr>
<td style="text-align:center">Agda</td>
<td style="text-align:center">Yes</td>
<td style="text-align:center">Haskell, JavaScript</td>
<td style="text-align:center"><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php" target="_blank" rel="nofollow noopener noreferrer">https://wiki.portal.chalmers.se/agda/pmwiki.php</a></td>
</tr>
<tr>
<td style="text-align:center">Vampire</td>
<td style="text-align:center"></td>
<td style="text-align:center"></td>
<td style="text-align:center"><a href="http://www.vprover.org" target="_blank" rel="nofollow noopener noreferrer">http://www.vprover.org</a></td>
</tr>
<tr>
<td style="text-align:center">TLA+</td>
<td style="text-align:center"></td>
<td style="text-align:center">Go<sup class="footnote-ref"><a href="#fn-991d-2" id="fnref-991d-2">[2]</a></sup>
</td>
<td style="text-align:center"><a href="http://lamport.azurewebsites.net/tla/tla.html" target="_blank" rel="nofollow noopener noreferrer">http://lamport.azurewebsites.net/tla/tla.html</a></td>
</tr>
<tr>
<td style="text-align:center">Idris</td>
<td style="text-align:center">Yes</td>
<td style="text-align:center"></td>
<td style="text-align:center"><a href="http://docs.idris-lang.org/en/latest/tutorial/theorems.html" target="_blank" rel="nofollow noopener noreferrer">http://docs.idris-lang.org/en/latest/tutorial/theorems.html</a></td>
</tr>
<tr>
<td style="text-align:center">Learn</td>
<td style="text-align:center">Yes</td>
<td style="text-align:center"></td>
<td style="text-align:center"><a href="http://leanprover.github.io" target="_blank" rel="nofollow noopener noreferrer">http://leanprover.github.io</a></td>
</tr>
<tr>
<td style="text-align:center">Cedille</td>
<td style="text-align:center">Yes</td>
<td style="text-align:center"></td>
<td style="text-align:center"><a href="https://cedille.github.io" target="_blank" rel="nofollow noopener noreferrer">https://cedille.github.io</a></td>
</tr>
</tbody>
</table>
<section class="footnotes">
<span class="footnotes-title">脚注</span>
<ol class="footnotes-list">
<li id="fn-991d-1" class="footnote-item">
<p>ここで Extraction は定理証明支援系のコードから他言語への変換機能のことを言っています｡ <a href="#fnref-991d-1" class="footnote-backref">↩︎</a></p>
</li>
<li id="fn-991d-2" class="footnote-item">
<p><a href="https://github.com/UBC-NSS/pgo" target="_blank" rel="nofollow noopener noreferrer">https://github.com/UBC-NSS/pgo</a> <a href="#fnref-991d-2" class="footnote-backref">↩︎</a></p>
</li>
</ol>
</section>


<p>取り敢えず思い浮かんだものを書き出した｡</p>


名前	依存型	Extraction^[1]	Link
Isabelle		Haskell, OCaml, SML, Scala	https://isabelle.in.tum.de
Coq	Yes	Haskell, OCaml, Scheme	https://coq.inria.fr
Agda	Yes	Haskell, JavaScript	https://wiki.portal.chalmers.se/agda/pmwiki.php
Vampire			http://www.vprover.org
TLA+		Go^[2]	http://lamport.azurewebsites.net/tla/tla.html
Idris	Yes		http://docs.idris-lang.org/en/latest/tutorial/theorems.html
Learn	Yes		http://leanprover.github.io
Cedille	Yes		https://cedille.github.io