Pure Type System 教程:从基础到进阶
本教程为读者提供一个从基础到进阶的 Pure Type System 学习路径,涵盖 PTS 核心定义、λ-Cube 谱系、构造演算 CoC、归纳构造演算 CIC,以及 Curry-Howard 同构。
本教程为读者提供一个从基础到进阶的 Pure Type System 学习路径,涵盖 PTS 核心定义、λ-Cube 谱系、构造演算 CoC、归纳构造演算 CIC,以及 Curry-Howard 同构。
De Bruijn 索引是一种在 lambda 演算和形式化逻辑中用于表示变量绑定的方法,它用数字代替变量名,消除了变量名冲突和 α-等价的麻烦。
CIC(Calculus of Inductive Constructions)是现代交互式定理证明器的核心理论基础。它在 CoC 的基础上增加了归纳类型,统一地表达程序、数学命题和证明。
完成了 AgentMoss v1.2.1 的跨平台 Hook 监控适配,支持 OpenClaw、xiaoO、HERMES、JiuwenClaw 四个平台的 hook 对接。三层行为图建模(CFG/DFG/PDG)的基础结构已经稳定,61 条威胁检测规则覆盖了数据泄露、凭证窃取、命令注入等 11 个类别。 核心挑战在于不...
新开了文学板块,把公众号的 40 篇文章全部迁移到了博客。技术上复用了 posts 的数据类型和渲染逻辑,新增了 literatureDirectory 和 getAllLiterature 函数,路由结构保持 /literature/[slug] 的一致性。 比较有意思的一点是 TypeScript 里 slugRe...
作者 Antonio Gulli
全面介绍 Agentic 设计模式,从基础的 Prompt Chaining、Routing 到高级的 Multi-Agent Collaboration、Reasoning Techniques,涵盖 21 个核心设计模式及实践代码示例。
作者 Flemming Nielson, Hanne R. Nielson, Chris Hankin
系统介绍程序分析的理论基础与实践方法,适合研究生和研究人员阅读。
作者 Edmund M. Clarke, Orna Grumberg, Doron A. Peled
全面介绍模型检验的理论与实践,是学习形式化验证的经典教材。