diff --git a/content/多段階計算.md b/content/多段階計算.md
index 28f39ad7..a70048ee 100644
--- a/content/多段階計算.md
+++ b/content/多段階計算.md
@@ -31,3 +31,12 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
 ## 依存型との組み合わせ
 
 [A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)
+
+https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4
+
+> Let’s consider an application, for example, in computer graphics, in which we have potentially many pairs of vectors of the fixed (but statically unknown) length and a function—such as vector addition—to be applied to them. 
+> This function should be fast because it is applied many times and be safe because just one runtime error may ruin the whole long-running calculation. 
+> Our goal is to define the function `vadd` of type $$Πn : Int.∀β.⊲β(Vector (\%_αn) → Vector (\%_αn) → Vector (\%_αn))$$
+> .It takes the length n and returns (β-closed) code of a function to add two vectors of length n. The generated code is run by applying it to ε to obtain a function of type $Vector\; n → Vector\; n → Vector\; n$ as expected.
+
+この辺はなんかやりたいことに近そうな予感がする
\ No newline at end of file