계획된 문서

[damhiya]

프로그래밍 언어

• [ ] C
• [ ] C++
• [x] Rust
• [ ] ML
• [ ] Standard ML
• [ ] OCaml
• [x] Coq
• [ ] Prolog

프로그래밍 언어 이론

• [x] λ 계산
• [x] STLC
• [ ] strictness
• [ ] eager / lazy evaluation
• [ ] operational semantics
• [ ] denotational semantics
• [ ] small-step semantics
• [ ] big-step semantics
• [ ] evaluation
• [ ] normalization
• [ ] hereditary substitution
• [ ] undefined behavior
• [ ] Hindley-Milner type system
• [ ] Bidirectional typing

프로그램 검증

• [x] Hoare logic
• [x] Separation logic
• [ ] Simulation
• [ ] Refinement
• [ ] Interaction tree

논리학

• [x] 배중률
• [ ] 1st order logic
• [ ] Intuitionistic logic
• [ ] Linear logic
• [ ] Affine logic
• [ ] Modal logic
• [ ] Cut-elimination theorem
• [ ] 명제
• [ ] 판단(judgement)
• [ ] hypothetical judgement

타입 이론

• [ ] Inductive type
• [ ] Coinductive type
• [ ] CoC
• [ ] CIC
• [ ] HoTT
• [ ] Girard의 역설
• [ ] Curry의 역설

수학

• [x] 러셀의 역설
• [x] 원순서
• [x] 부분순서
• [ ] 전순서
• [x] 동치관계
• [x] Knaster-Tarski 정리
• [x] 카테고리
• [ ] 함자
• [ ] 자연변환
• [ ] Polynomial functor