A study on denotational semantics of λμ-calculus
| Project/Area Number |
14540119
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Gunma University (2004)
Shimane University (2002-2003) |
|---|
Principal Investigator |
FUJITA Ken-etsu Gunma University, Department of Computer Science, Associate Professor, 工学部, 助教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KONDO Michio Tokyo Denki University, School of Information Environment, Professor, 情報環境学部, 教授 (40211916)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2003: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2002: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | λμ-calculus / CPS-translation (continuation) / Polymorphic functions / Abstract data types / Curry-Howard isomorphism / Galois connection / Control operator / Duality / CPS変換 / 表示的意味論 / 継続 / スコット領域 / Cモノイド / タイプフリーラムダミュウ計算 / 継続的意味論 / タイプフリーラムダ計算 / 不動点演算子 / 完備半順序集合(CPO) |
|---|
| Research Abstract |
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.
|
Report
(4 results)
Research Products
(17 results)
