Bring mutable state into denotational semantics by modeling locations, stores, expressions, and commands in a typed lambda calculus with effects.

Turn domain theory into a working semantics for PCF, using factorial, multiple fixed points, and fixed-point induction to reason about recursive programs.

Discover how fixed points support recursive definitions and how continuous domains assemble into a full hierarchy for interpreting higher-order types.

Prepare a semantic home for recursion through partial orders, complete partial orders, continuous functions, and function spaces that are themselves CPOs.

How can typed lambda terms receive mathematical meaning? Build Henkin-style models from applicative structures, frames, environments, and soundness conditions.

五篇类型化 Lambda 演算指称语义笔记的中文导航，从 Henkin 模型、CPO 与连续函数走向 PCF 和命令式程序模型。

Move from functional models to imperative programs by formalizing locations, stores, expression evaluation, commands, and the operational semantics of While.

See algebraic data types through universal algebra, connecting signatures, terms, equations, interpretations, and proof systems in one coherent framework.

What does the turnstile symbol really claim? Explore equations, theories, derivations, and the proof systems that make formal judgments trustworthy.

Tour the eight PLDI 2023 Distinguished Papers and their ideas in verification, compilers, proof repair, synthesis, and quantum circuit analysis.