The type inference algorithm always plays an important role in …

  之前在群里和群友讨论，如果你不打算搞纯理论方向的研究，那么学习理论知识究竟有什么意义，就拿计算机语言说事，看上去现在的绝大部分 …

Theoretical Foundation of Typechecking Algorithm for Equi-Recursi …

The Proof of Knaster-Tarski Theorem Definition[Monotone Function] …

对物语系列主角的思考——阿良良木历的虚伪从何而来   从终物语的剧情来看，阿良良木历拥有一个非常扭曲的人格，混合了自我厌恶，排外和 …

  我怀着非常生气的心情写下这篇文章，因为为了解决这个问题我毁掉了自己的生产环境。   在 …

Subtyping   We use \tau <: \sigma to denote that \tau is a sub …

Strong Normalization of Simply Typed Lambda Calculus   From the ( …

Preliminaries The Typing Relation   A term t belongs to type T me …

  The syntax of Church’s lambda calculus can be described by BNF: ̷