A study on denotational semantics of λμ-calculus

直觉主义逻辑和类型化λ-演算之间的对应被称为Curry-Howard同构。M.Parigot（1992）扩展了对应关系，并引入λμ-演算作为二阶经典逻辑。λμ-演算是λ-演算的自然扩展，系统本身作为函数计算模型是非常有趣的。在过去的两年中，我们研究了以下几个问题：（1）从无类型和简单类型的λμ-演算到λ-演算的CPS-翻译;（2）λμ-演算和C-幺半群的延拓指称语义;（3）CPS-翻译与延拓指称语义在CPO上的相似关系。证明了多态λ-演算与λ-演算的一个子系统之间存在双射变换，它们构成一个Galois联络，进而构成一个Galois嵌入.从编程的角度来看，这个结果意味着多态函数可以用抽象数据类型表示。

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.