A categorical semantic for the Typed Epsilon Calculus

Typed Hilbert Epsilon Operators and the Semantics of Determiner Phrases (Invited Lecture)

The semantics of determiner phrases, be they definite de- scriptions, indefinite descriptions or quantified noun phrases, is often as- sumed to be a fully solved question: common nouns are properties, and determiners are generalised quantifiers that apply to two predicates: the property corresponding to the common noun and the one corresponding to the verb phrase. We first present a criticism of this standard view. Firstly, the semantics of determiners does not follow the syntactical structure of the sentence. Secondly the standard interpretation of the indefinite article cannot ac- count for …

薄ε超教义的内部语言：可靠性、完备性与Rocq形式化

Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization

该研究提出带希尔伯特ε算子的直觉主义内涵一阶逻辑的类型化证明项演算，证明其关于特定超教义模型的可靠性与完备性，相关成果在Rocq中形式化。

形式语义学中类型化外延与内涵模型的范畴框架

Categorical Framework for Typed Extensional and Intensional Models in Formal Semantics

本文用范畴论统一表示形式语义学中的类型化外延与内涵模型，构造内涵模型范畴 ModInt，证明平凡内涵模型等价于外延模型，为处理内涵与恢复外延提供模块化且与顺序无关的方法。

类型化线性代数 lambda 演算的具体模型

A concrete model for a typed linear algebraic lambda calculus

本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。

Curry-Howard-Lambek Correspondence for Intuitionistic Belief

This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $λ$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using that interpretation, it is also proved that $\mathsf{IEL}^{-}$ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in $\mathsf{IEL}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.

依赖类型理论带计算公理语义的2-范畴方法

A 2-categorical approach to the semantics of dependent type theory with computation axioms

本文用2-范畴方法为带计算公理的依赖类型理论建立语义，证明其类型构造子可编码为显示映射2-范畴，并语义证明内涵恒等类型的计算规则不可采纳。