型理論

• Calculus of Constructions
• Existential Type
• Higher-kinded types
• HM型推論をJuliaで実装する
• POPL2013, PEPM2013, PLMW2013報告
• Structural Subtyping
• Subtyping Overview and Implementation
• System F
• カインド
• ラムダキューブ
• 依存型
• 20211214_型クラス
• 型理論
• 多段階計算
• 代数的データ型
• Simply Typed Lambda Calculus
• 変性
• 篩型

2021-08-09

• 自作言語の型システムの話 - Qiita
  • term 線形論理
  • 私と型システムとポエム

「型のある言語は型を書く必要がある」
一番良く見るやつ。戦犯度が高い。二度とその口を開くなという気持ちになる。

草

• Rust は リージョン推論を取り入れている

  • リージョン.= ブロック → ライフタイム

• term 半知半解

• repo: wakame-tech/type-theory-rs

  • Algorithm W
  • Untyped Lambda-Calculus interpreter
  • Subtyping Overview and Implementation
  • Structural Subtyping

• TaPL