Research on Programming Language Design Theory Based on Type Theory

基于类型论的程序设计语言设计理论研究

• 批准号: 06680319
• 负责人: OHORI Atsushi
• 金额: $ 1.15万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1994
• 资助国家: 日本
• 起止时间: 1994 至 1995
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-06680319/
• 关键词: Type Theory; Programming Language; Compiler; Data Model; Polymorphism; 型推論

The purpose of this research is to develop a type theoretical foundation for designing a robust programming language that can be used for advanced software development. More specific goal of this research is to develop a foundation for compiling polymorphic programming language that support flexible record operations and the features of parallel and distributed processing.In the second year of this research, we have successfully completed one of the goal of a compilation theory for a polymorphic record calculus, and the result is published as an articleentitled "A Polymorphic Record Calculus and its Compilation" by A.Ohori in the November 1995 issue of ACM Transactions on Programming Languages and Systems. We have also developed a theory for efficient implementation of a polymorphic function, whose result is reported as an article "An Unboxed Semantics for ML Polymorphism" by A.Ohori and T.Takamizawa, which is submitted for publication.We believe that these results enables us to construct a practical compiler for a polymorphic language, and therefore that we have achieved the goal set for this research project. Jointly with Oki Electric Industry, co.Ltd, we are currently planing a two year compiler construction project based on the results obtained by this research.

本研究的目的是开发一个类型的理论基础，设计一个强大的编程语言，可用于先进的软件开发。更具体的目标是为支持灵活的记录操作和并行分布式处理的多态程序设计语言的编译奠定基础。在本研究的第二年，我们成功地完成了多态记录演算的编译理论的目标之一，其结果发表在1995年11月的ACM程序设计语言和系统学报上，题为“A Polymorphic Record Calculus and its Compilation”。我们还开发了一个理论，有效地实现了多态函数，其结果被报告的文章“一个Unboxed语义ML多态性”由A.Ohori和T.Takamizawa，这是提交出版。我们相信，这些结果使我们能够构建一个实用的编译器的多态语言，因此，我们已经实现了本研究项目的目标。我们与冲电气工业株式会社合作，目前正在计划一个基于本研究结果的为期两年的编译器构建项目。

项目成果

大堀 淳: "MLプログラミング入門(III)" コンピュータソフトウェア. 12(3). 3-14 (1995)

Atsushi Ohori：“机器学习编程简介（III）”计算机软件 12(3)。

A. Ohori: "A Polymorphic Record Calculus and Its Comp:lation" ACM Transactions on Programming Languages and Systems. 17. 844-895 (1995)

A. Ohori：“多态记录演算及其编译”ACM Transactions on 编程语言和系统。

Y. Minamide, G. Morriseft, R. Harper: "Typed Closure Conversion" Proceedings of the 23rd ACM Symposium of Programming Languages on Principles.(1995)

Y. Minamide、G. Morriseft、R. Harper：“类型化闭包转换”第 23 届 ACM 编程语言原理研讨会论文集。（1995 年）

I. Ulidowski: "Axionatizations of Weak Equivalences for De Simone Languages" Proceedings of the 6th International Conference in Concurrency Theory. 219-233 (1995)

I. Ulidowski：“De Simone 语言弱等价的轴离化”第六届并发理论国际会议论文集。

A.Ohori: "Introduction to ML Programmin (III)" Computer Software. 12(3). 3-14 (1995)

A.Ohori：《ML 程序简介（三）》计算机软件。