Open
Description
프로그래밍 언어
- C
- C++
- Rust
- ML
- Standard ML
- OCaml
- Coq
- Prolog
프로그래밍 언어 이론
- λ 계산
- STLC
- strictness
- eager / lazy evaluation
- operational semantics
- denotational semantics
- domain theory
- small-step semantics
- big-step semantics
- evaluation
- normalization
- hereditary substitution
- undefined behavior
- Hindley-Milner type system
- Bidirectional typing
- interaction tree
- cbpv
- Higher kinded type
- Higher rank polymorphism
- Polymorphic recursion
- type operator, type constructor, type former
프로그램 검증
- Hoare logic, weakest precondition
- Separation logic
- Simulation
- Refinement
- Interaction tree
논리학
- 배중률
- 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의 역설
- type constructor injectivity
- mutual induction
- inductive-recursive definition
- inductive-inductive definition
- induction scheme in Coq
수학
- 러셀의 역설
- 원순서
- 부분순서
- 전순서
- 동치관계
- Knaster-Tarski 정리
- 카테고리
- 함자
- 자연변환
- Polynomial functor
Metadata
Metadata
Assignees
Labels
No labels