19 lines
1.1 KiB
Markdown
19 lines
1.1 KiB
Markdown
|
#paper #programming-language
|
|||
|
|
|
|||
|
|
https://dl.acm.org/doi/10.1145/3471872.3472970
|
|||
|
|
|
|||
|
|
ラムダ計算に`feed`という1サンプルフィードバックを導入する形式を取る
|
|||
|
|
|
|||
|
|
[[mimium]]で`self`を使って1サンプルフィードバックができる、というのと近い（ちょうどmimiumと同じカンファレンスで発表された）
|
|||
|
|
|
|||
|
|
ただし対象は線形時不変システムの形式化で、異なるトポロジーのフィルターが最終的に同一のものであるのが証明できたりすると嬉しいよね、みたいなモチベだと理解してる（なので、項同士の加算は定義されているが、乗算は項と定数のみに制限されている）
|
|||
|
|
|
|||
|
|
|
|||
|
|
[[Coq]]で証明が実装されている https://github.com/ejgallego/mini-wagner-coq/
|
|||
|
|
|
|||
|
|
よく見たらこのAuthorの[[Emilio Jesús Gallego Arias]]、Coq本体の開発をゴリゴリやってる人だ（強いわけだ）
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
実際に動かすためのコンパイラは[[MetaOCaml]]とかを使っている（なんかプログラムを一度蒸留するとリアルタム動作するものが出てくる、的な雰囲気だったはず）
|