[obsidian] vault backup: 2025-12-19 15:28:06[

content/Coqの勉強.md

@@ -3,7 +3,7 @@ date: "2023-08-24T21:45:03+0900"
 ---
 #programming-language #memo #logic
 
-[[Coq]]を用いた定理証明支援の基礎
+[[Coq]]を用いた[[定理証明支援]]の基礎
 
 - [Software Foundations 日本語訳](https://chiguri.info/sfja/)
 	- 大体これ読めばいいっぽい（プログラミング言語系は特に）
@@ -22,12 +22,12 @@ date: "2023-08-24T21:45:03+0900"
 
 ・・・というのは全部、あくまで普通の関数型言語で考えたら、というので、厳密には全然違う
 
-問題はCoqがラムダキューブ最上位のCalculus of Constructionを採用しているところ。つまり次の全てが扱える
+問題はCoqがラムダキューブ最上位の[[Calculus of Construction]]を採用しているところ。つまり次の全てが扱える
 
 - 項に依存する項 単純型付ラムダ計算
 - 型に依存する項（ジェネリクス）System F
 - 型に依存する型（カインド多相）System F $\underline{\omega}$
-- 型依存の型と型依存の項の両方 System F$\omega$
+- 型依存の型と型依存の項の両方 [[System-Fω]]
 - 項に依存する型（依存型） $\lambda\Pi$
 - 型依存の項と依存型　$\lambda\Pi2$
 - 型依存の項、項依存の型、型依存の項 CoC