A study on denotational semantics of λμ-calculus

直觉主义逻辑和类型化λ演算之间的对应关系被称为CurryHoward同构。M.Parigot(1992)推广了对应关系，并引入λμ演算作为二阶经典逻辑。λμ演算是λ演算的自然扩展，系统本身作为函数计算模型非常有趣。在过去两年的项目中，我们研究了以下几点：(1)无类型和简单类型的λμ演算到λ演算的CP-翻译；(2)λμ演算和C-么半群的延续指称语义；(3)CP-翻译和延续指称语义之间的相似关系。为了扩展上述结果，我们引入了一个新的系统--存在类型系统λ∃。证明了多态λ演算与λ∃的一个子系统之间存在双射变换，从而形成了伽罗瓦连接，进而形成了伽罗瓦嵌入。从编程的角度来看，这一结果意味着多态函数可以由抽象数据类型表示。

A correspondence between Intuitionistic logic and typed λ-calculus is well-known as Curry-Howard isomorphism. M.Parigot (1992) has extended the correspondence and introduced λμ-calculus as a second-order classical logic. λμ-calculus is a natural extension of λ-calculus and the system itself is quite interesting as a functional computation model. In the last two years' project, we have investigated the following points :(1)CPS-translation from type-free and simply typed λμ-calculi intoλ-calculus ;(2)Continuation denotational semantics of λμ-calculus and C-monoid ;(3)Similarity relation on CPO between CPS-translation and continuation denotational semantics.In order to extend the results above, we introduced a new system, an existential type system λ∃. It is proved that there exist bijective translations between polymorphicλ-calculus and a subsystem of λ∃, which form a Galois connection and moreover Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.