Abstract: This paper briefly introduces Coquand and Huet's Calculus of Constructions (CC) and a Framework for Binding Operators (FBO). It then shows CC's axiomatization in FBO. This axiomatization is without an infinite type hierarchy. Specifically, we introduce an extra universe kind above the original universe type in CC. But we allow neither quantification over kind nor introduction of y: kind. Another operator=> is added for typing II types in FBO, since we are only considering a single-sorted FBO. Technically speaking, we translate CC into FBO; i.e. every CC term is typed in FBO. For example, II,i>x:M.N in CC is translated as IIy.u:t=>v in FBO, where x, M and N correspond to y, t and u respectively under the translation. As a result, we demonstrate that FBO is powerful enough to provide an equational platform for CC.

Key words: binding opera tors, a Framework for Binding Operators (FBO), equational logics, axiomatization, Calculus of Constructions (CC)

摘要： 首先简略介绍Coquand和Huet的构造演算以及Plotkin和孙踊的受囿算子系统。然后，将构造演算在受囿算子系统中进行公理化。此公理化无需无限级(数据)类型结构。原则上，可以在原构造演算的type空间之上引入kind空间。但是，不允许在kind上使用量词，也不允许引入y: kind。从技术上说，将忠实地把构造演算翻译进受囿算子系统中去。为了能对构造演算中的Π类型受予受囿算子系统中的类型，不得不引入新的=>算子。举例来说，构造演算中的Πx:M.N可用受囿算子系统中的Πy.u:t=>v来表达。其中，x对应于y, M对应于t，以及N对应于u。其结果是受囿算子系统具有足够的能力为构造演算提供一个等值逻辑演算环境。

关键词: 受囿算子系统, 等值逻辑, 公理化, 构造演算, 受囿算子