From aa71637fe64effaa246606b71d00e3f6aee5ea72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Fri, 11 Jul 2025 13:08:46 +0900 Subject: [PATCH] [obsidian] vault backup: 2025-07-11 13:08:46[ --- content/多段階計算.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/content/多段階計算.md b/content/多段階計算.md index 342dda25..ecef8095 100644 --- a/content/多段階計算.md +++ b/content/多段階計算.md @@ -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) +## 用語 + +**Cross-Stage Persistence**：基本的にステージ0/1でのコードはそれぞれステージ0/1の中でしか使えない。何らかの方法で両方のステージで跨いで使える仕組みを作れると便利 + +**Run**プリミティブ： + ## [[依存型]]との組み合わせ [A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)