diff --git a/content/Coqの勉強.md b/content/Coqの勉強.md index 49b7e0b8..38bbab5a 100644 --- a/content/Coqの勉強.md +++ b/content/Coqの勉強.md @@ -8,6 +8,7 @@ - 神戸大学 [Coq による定理証明入門 髙橋真(2023)](http://herb.h.kobe-u.ac.jp/coq/coq.pdf) - 千葉大学大学院 [定理証明支援系 Coq での 論理的なリーゾニング 集中講義 アフェルト レナルド(2017)](https://staff.aist.go.jp/reynald.affeldt/coq/riron.pdf) - IIJ技術研究所 [Coq を始めよう 池渕未来(2011)](https://www.iijlab.net/activities/programming-coq/coqt1.html) +- [Real World Coq – An introduction to effective theorem proving](https://ejgallego.github.io/real-world-coq/) by [[Emilio Jesús Gallego Arias]] ## 備忘録 - `Inductive`が変数宣言 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 index 94a8b1a5..629edcd5 100644 --- 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 @@ -2,6 +2,8 @@ https://dl.acm.org/doi/10.1145/3471872.3472970 +first author: [[Emilio Jesús Gallego Arias]] + ## 概要 ラムダ計算に`feed`という1サンプルフィードバックを導入する形式を取る @@ -46,6 +48,43 @@ and machine : type a . int → a expr → env → a = |... ``` +ただし、リポジトリのCoqのコードでは別に相互再帰で実装されてるわけではない + +```ocaml +Definition exprI n (pI : I n) : I n.+1 := + fix eI k hk {Γ t} e {struct e} := + match e in expr Γ t return env k Γ -> tyI k t with + | var v Γ idx => fun Θ => nth (I0 k _) (hnth (hist0 k _) v Θ) idx + | add _ _ e1 e2 => fun Θ => eI k hk e1 Θ + eI k hk e2 Θ + | mul _ _ c e => fun Θ => c *: eI k hk e Θ + | pair _ _ _ e1 e2 => fun Θ => col_mx (eI k hk e1 Θ) (eI k hk e2 Θ) + | proj m _ i e => fun Θ => \col__ (eI k hk e Θ) i ord0 + | lam m _ _ e => fun Θ v => eI k hk e (v, Θ) + | app _ _ _ ef ea => fun Θ => + let efI : tyI k (tfun _ _) := eI k hk ef Θ in + let eaI : hist k _ := + accI (fun k hk => eI k hk ea) hk Θ in + efI eaI + | feed tn Γ e => fun Θ => + let prev := + accF (fun k hk => pI k hk _ _ (feed e)) hk Θ in + eI k hk e (prev, Θ) + end. + +(* Need to prove |acc_feed n.+1| = acc_norm n ?? *) + +(* We build our step-indexed representation *) +Fixpoint exprIn n {struct n} : I n.+1 := + match n return I n.+1 with + | 0 => fun k hk Γ t e (Θ : env k Γ) => + exprI (@IE0 _) hk e Θ + | n.+1 => fun k hk Γ t e (Θ : env k Γ) => + exprI (@exprIn n) hk e Θ + end. + +``` + +そしてCoqで証明されているのはここまで(MetaOCamlのReal-World exampleが欲しいよ) #### B:Imperativeなインタプリタ diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md index 584c6086..531338bc 100644 --- a/content/音楽プログラミング言語の形式化.md +++ b/content/音楽プログラミング言語の形式化.md @@ -1,7 +1,7 @@ #programming-language #research -## 先行令 +## 先行例 [[Faust]]