[obsidian] vault backup: 2026-01-29 12:55:09[

content/多段階計算.md

@@ -16,7 +16,7 @@ https://logmi.jp/tech/articles/324146
 MetaOCaml を使った自己反映言語のコンパイル 浅井 健一  (Black )
 http://www.is.ocha.ac.jp/~asai/jpapers/ppl/asai14.pdf
 
-メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 五十嵐 淳
+メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 [[五十嵐淳]]
 http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/pdf/lambdaCB-PPL05.pdf
 
 筑波大学　論理と計算（2）
@@ -42,7 +42,21 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
 
 **Cross-Stage Persistence**：基本的にステージ0/1でのコードはそれぞれステージ0/1の中でしか使えない。何らかの方法で両方のステージで跨いで使える仕組みを作れると便利
 
-**Run**プリミティブ：
+[multi-stage-programs-in-context.pdf](https://mpickering.github.io/papers/multi-stage-programs-in-context.pdf)
+
+Path Based Persistence: グローバルレベルで定義されたシンボルはどのステージでも使えるようにする
+
+Serialisation-based persistence
+
+各プリミティブにliftという関数を用意して、値→値リテラルのコードを変換できるようにする。構造体などは各フィールドを再帰的にliftしたものになる。
+
+問題は関数丸ごとリフトするような一般的な方法がないことである。
+
+例えばこんなコードだったら
+
+``let x = `(x+1) ``
+
+``let x = `($(lift(x) + 1))` ``であってほしい。これは構文木を再帰的に辿れば一応できそう
 
 ## [[依存型]]との組み合わせ
 
@@ -58,6 +72,15 @@ https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4
 この辺はなんかやりたいことに近そうな予感がする
 
 
+## [[モジュール]]システムとの組み合わせ
+
+[A Research Talk at FLOPS 2024: An ML-Style Module System for Cross-Stage Type Abstraction in Multi-Stage Programs - gfnweb](https://gfngfn.github.io/posts/2024-05-18-slides-flops2024/)
+
+[[Suwa Takashi]] 
+
+
+
+
 ## [[Rust]]でのプログラム合成
 
 https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html