[Update: 2025/04/10]

My notes piles up here.
For now, pasted notes are all written in [zh-CN].

• [zh-CN] 音乐理论系列

  1. 音符 pdf@20250111
     音符、音名、唱名、和弦.
  2. 吉他 pdf@20250111
     吉他标准调弦、自然大调、调内和弦.

• [zh-CN] 自动摊还资源分析 pdf@20240614
  对 Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis, the thesis by Jan Hoffmann 的学习, 当初写来主要是为了更加熟悉资源分析, 其实我到现在对多变量多项式也还不是很熟悉, 也许之后还会更新一版.

• [zh-CN] 模态逻辑 pdf@20240413
  本文介绍了一些正规模态逻辑系统以及他们的关系. 本文首先定义Kripke语义, 然后再引入推理规则, 但略去了 Soundness/Completeness 的证明. 本文原欲给出一个自然演绎系统, 然而无暇处理meta theory, 便只是套了个这么框架; 模态逻辑系统内的定理证明, 使用推理树和交换图表两种形式, 后者(对于了解范畴论语言的读者)更直观.

• [zh-CN] Martin Löf 类型论 pdf@20230703
  本文是 ∞-type Café 暑期学校 2023 中关于依值类型论入门的部分, 实际上介绍的是一种内蕴 Martin Löf 类型论 (Intensional Martin Löf Type Theory).