Call-By-Push-Value

/icons/hr.icon

description

計算モデル．普通の関数型(項書換えや項代数，項言語を使ったもの)の拡張．←と違って，データと計算とか，式と文とかを区別している(lamdba は全部lambda式)．

なんかmonadと線形論理の関係について話してそう．(effectの観点から)

value type とcomputational typeの定義がよくわからん．