証明モナド

• https://www.sciencedirect.com/science/article/pii/S1567832610000068 The proof monad, 14p。対話的手続き的証明系のモナド定式化。ローカルに落とした、~/archive/ProofMonads.pdf

これ読んでみたが、予想と違うことが書いてあった。証明モナドはモッジの意味の計算的モナドで、手続き的タクティク言語による証明支援系のインタプリタとしての動作を説明するモナドだった。

が、前半は非常に参考になった。僕はタクティク言語はまったく考えてなくて記述言語／文書化言語〈description/documentation language〉を考えているが、論理式、シーケント、シーケント推論、シーケント推論の変形という 0, 1, 2, 3 射があることはハッキリした。