『依存型を含むマルチステージプログラミングの型理論』 - pogi-log

『依存型を含むマルチステージプログラミングの型理論』

依存型を含むマルチステージプログラミングの型理論. 2018.

bracket，escape，run，cross-stage persistence(CSP)

マルチステージプログラミングというものがある

依存型は値に依存する型

依存型の応用例

配列外参照の防止

型付きラムダ計算

『MetaML and Multi-stage Programming with Explicit Annotations』

『Eliminating Array Bound Checking Through Dependent Types』

#論文 #型理論 #論文読み