From 8e2bf1e498de56da8b8be4f5ce6621153af24f60 Mon Sep 17 00:00:00 2001 From: "Tomoya Matsuura(MacBookPro)" Date: Tue, 22 Aug 2023 23:39:29 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-08-22 23:39:29[ --- content/Coq.md | 3 +++ content/Emilio Jesús Gallego Arias.md | 6 ++++++ content/Faust.md | 3 +++ ... of digital signal processing algorithms.md | 18 ++++++++++++++++++ content/五十嵐淳.md | 1 + content/音楽プログラミング言語.md | 4 +++- content/音楽プログラミング言語の形式化.md | 12 ++++++++++++ 7 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 content/Coq.md create mode 100644 content/Emilio Jesús Gallego Arias.md create mode 100644 content/Faust.md create mode 100644 content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md create mode 100644 content/五十嵐淳.md create mode 100644 content/音楽プログラミング言語の形式化.md diff --git a/content/Coq.md b/content/Coq.md new file mode 100644 index 00000000..f3ee5b99 --- /dev/null +++ b/content/Coq.md @@ -0,0 +1,3 @@ +#tools #software + +定理証明支援システム \ No newline at end of file diff --git a/content/Emilio Jesús Gallego Arias.md b/content/Emilio Jesús Gallego Arias.md new file mode 100644 index 00000000..c711afef --- /dev/null +++ b/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/ + diff --git a/content/Faust.md b/content/Faust.md new file mode 100644 index 00000000..23b53963 --- /dev/null +++ b/content/Faust.md @@ -0,0 +1,3 @@ +#software #programming-language #sound + +https://faust.grame.fr \ No newline at end of file diff --git a/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md b/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md new file mode 100644 index 00000000..33df10a0 --- /dev/null +++ b/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]]とかを使っている（なんかプログラムを一度蒸留するとリアルタム動作するものが出てくる、的な雰囲気だったはず） diff --git a/content/五十嵐淳.md b/content/五十嵐淳.md new file mode 100644 index 00000000..bcfd8cf8 --- /dev/null +++ b/content/五十嵐淳.md @@ -0,0 +1 @@ +#person \ No newline at end of file diff --git a/content/音楽プログラミング言語.md b/content/音楽プログラミング言語.md index 45f03dd1..841a5178 100644 --- a/content/音楽プログラミング言語.md +++ b/content/音楽プログラミング言語.md @@ -7,4 +7,6 @@ --- -音楽プログラミング言語に[[多段階計算]]を導入できないかのメモ \ No newline at end of file +[[音楽プログラミング言語の形式化]] + +[[多段階計算]] \ No newline at end of file diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md new file mode 100644 index 00000000..046d6aa6 --- /dev/null +++ b/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]] \ No newline at end of file