Blog

Posts are grouped by topic and sorted by publication date automatically. Topics may contain nested subcategories.

Agent Design

• A Programming Paradigm for Spatiotemporal Composability (2026-08-15)

  论文 "A Programming Paradigm for Spatiotemporal Composability" 的中英双语对照翻译，提出了一种面向时空可组合性的编程范式，通过将经典效应与协效应概念提升为运行时机制，实现动态组合的形式化基础。

• Demystifying evals for AI agents (2026-08-13)

  Anthropic 原文 "Demystifying evals for AI agents" 的中英双语对照翻译，涵盖 AI 智能体评估的核心概念、评估器类型、评估流程和最佳实践。

• Quantifying infrastructure noise in agentic coding evals (2026-08-13)

  Anthropic 原文 "Quantifying infrastructure noise in agentic coding evals" 的中英双语对照翻译，探讨基础设施配置如何影响智能体编码评估的结果。

• Understanding Rethlas and Archon (2026-08-07)

  An overview of the Rethlas and Archon and their design principles.

• Understanding mini-swe-agent (2026-06-12)

  An overview of the mini-swe-agent and its design principles.

Book Notes

• Category Theory for Programmers 1-7 (2026-09-14)

  Notes on Category Theory for Programmers, chapters 1-7.

MLSys

15-779

• CMU 15-779 08-Tile-based DSL (2026-09-16)

  Notes for CMU 15-779 08-Tile-based DSL

• CMU 15-779 05-Wrap Specialization (2026-09-02)

  Notes for CMU 15-779 05-Wrap Specialization

• CMU 15-779 03-CUDA programming 2 (2026-08-13)

  Notes for CMU 15-779 03-CUDA programming 2

• CMU 15-779 04-Transformers, Attention, and FlashAttention (2026-08-13)

  Notes for CMU 15-779 04-Transformers, Attention, and FlashAttention

• CMU 15-779 03-CUDA programming 1 (2026-07-31)

  Notes for CMU 15-779 03-CUDA programming 1

• CMU 15-779 02-basics (2026-07-24)

  Notes for CMU 15-779 02-basics

Program Verification

• prove cbrt in CORE-MATH (2026-09-05)

  CORE-MATH 论文《Correctly Rounded Cubic Root Evaluation in Double Precision》的中英双语对照翻译，涵盖正确舍入立方根的算法设计、补偿算法精化、舍入测试与舍入误差分析。

• GLM-5.2 proves type punning in C (2026-08-10)

  展示 GLM-5.2 如何利用 CompCert 证明 C 语言中的类型双关。

• cbrt in musl (2026-08-05)

  An explanation of the cube root implementation in the musl C library.

• Formal verification of floating point trigonometric functions (2026-05-01)

  Paper reading notes on the formal verification of floating point trigonometric functions using HOL Light.

• k-induction (2026-04-22)

  Introduction to k-induction in program verification.