あきるor諦めるまでTaPLを定理証明支援系で形式化をします。
使用言語:Coq, Lean3
パーサー付きのものもある。
〜chap8 :The Coq Proof Assistant:version 8.11.2
chap9〜10:The Coq Proof Assistant:version 8.12.0
chap11〜 :The Coq Proof Assistant:version 8.13.0
- Chap.3(arith)
- Chap.4(arith)
- Chap.5(untype_lambda)
- Chap.6(untype_lambda)
- Chap.7(untype_lambda)(他のリポジトリでやった)
- Chap.8(typeArith)
- Chap.9(hastype_lambda/typeLambda_string)(パーサーなし)
- Chap.10(hastype_lambda/deBruijn)(パーサーなし)
- Chap.11(fullsimpl/chap11)(パーサーなし)
- Chap.22(recon/)(パーサーなし)
- Chap.23(systemF/chap23.v)