1.1 KiB
1.1 KiB
#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とかを使っている（なんかプログラムを一度蒸留するとリアルタム動作するものが出てくる、的な雰囲気だったはず）