[obsidian] vault backup: 2023-08-22 23:39:29[

content/Coq.md

@@ -0,0 +1,3 @@
+#tools #software 
+
+定理証明支援システム

content/Emilio Jesús Gallego Arias.md

@@ -0,0 +1,6 @@
+#person 
+
+[[Coq]]の開発とか[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms|W-calculus]]とか[[Faust]]の形式的証明プロジェクトとかやってらっしゃる
+
+https://www.irif.fr/~gallego/
+

content/Faust.md

@@ -0,0 +1,3 @@
+#software #programming-language #sound 
+
+https://faust.grame.fr

content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md

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

content/五十嵐淳.md

@@ -0,0 +1 @@
+#person 

content/音楽プログラミング言語.md

@@ -7,4 +7,6 @@
 
 ---
 
-音楽プログラミング言語に[[多段階計算]]を導入できないかのメモ
+[[音楽プログラミング言語の形式化]]
+
+[[多段階計算]]

content/音楽プログラミング言語の形式化.md

@@ -0,0 +1,12 @@
+#programming-language #research 
+
+[[Coq]]を用いた定理証明支援の基礎
+
+[Software Foundations 日本語訳](https://chiguri.info/sfja/)
+
+京都大学　[[五十嵐淳]] 「計算と論理」　授業資料(2023)
+
+https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/
+
+
+[[The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms]]