tomoyanonymous/quartz-research-note
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

[obsidian] vault backup: 2025-07-11 13:08:46[
All checks were successful
Build / build (push) Successful in 7m55s
Details

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya
2025-07-11 13:08:46 +09:00
parent 3dbbb6da30
commit aa71637fe6
1 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
content/多段階計算.md
View File

@@ -32,9 +32,18 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
λ○□：両方を統合 λ○□：両方を統合
[[SATySFi]]：組版言語だが、マクロのシステムとして多段階計算が導入されている。
[多段階計算の型システムの基礎 - gfnweb](https://gfngfn.github.io/ja/posts/2022-05-12-slides-type-system-matsuri-2020/)([[Suwa Takashi]])
[SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024) [SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024)
## 用語
**Cross-Stage Persistence**：基本的にステージ0/1でのコードはそれぞれステージ0/1の中でしか使えない。何らかの方法で両方のステージで跨いで使える仕組みを作れると便利
**Run**プリミティブ：
## [[依存型]]との組み合わせ ## [[依存型]]との組み合わせ
[A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035) [A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)