動的型付けと静的型付けを融合した漸進的型付けのメタ理論

结合动态和静态类型的渐进类型元理论

• 批准号: 19K20247
• 负责人: 関山 太朗
• 金额: $ 2.66万
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K20247/
• 关键词: プログラミング言語; 漸進的型付け; 多相性; 型システム; 継続渡し形式; 漸進的型システム; 計算効果

【多相性をもつ漸進的型付き言語】前年度までに引き続き、多相性を含む漸進的型付き言語の実装モデルである多相コアーション計算体系の、特に空間効率についての理論研究を行った。これまでの研究成果で多相性における重要な性質であるパラメトリシティと空間効率の良い実装が両立しないことは判明していたが、本年度は新たにその原因が名前生成の機構にあることを理論的に示した。また逆に、パラメトリシティを（完全にではないが）ある程度あきらめることで、多相性を含む漸進的型付き言語を空間的に効率良く実装するための知見を得た。【データ構造のための漸進的型付け】これまでにも様々なデータ構造を扱うために、列多相性をサポートする漸進的型付き言語の研究に取り組んできた。しかしこれまで考えていた列多相性はフィールド名の重複を許すものであったため、型上で表現された列構造の動的検査のための仕組みが想定以上に複雑になってしまっていた。そこで本年度では重複を許さない列多相を対象とした漸進的型付き言語の設計を行った。その結果、実行検査の仕組みが簡便になる見通しを得た。

[Multi-phase and Progressive Speech] The previous year, the introduction of multi-phase and progressive speech, the implementation of multi-phase and multi-phase computing systems, special spatial efficiency and theoretical research. The results of this study are important for the determination of the causes of polyphase and spatial efficiency. The degree of multi-phase, multi-phase, multi-phase The structure of the speech is gradually changed. The structure of the column is characterized by the repetition of the name of the column and the shape of the column. This year's multi-phase design The results of the survey and the results of the survey are simple and easy to understand.

项目成果

Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces

• DOI: 10.1609/aaai.v34i04.5977
• 发表时间: 2019-04
• 期刊: ArXiv
• 作者: Takamasa Okudono;Masaki Waga;Taro Sekiyama;I. Hasuo

Toward Neural-Network-Guided Program Synthesis and Verification

• DOI: 10.1007/978-3-030-88806-0_12
• 发表时间: 2021-03
• 作者: N. Kobayashi;Taro Sekiyama;Issei Sato;Hiroshi Unno

分岐付き確率的プログラミング言語の実現に向けて

实现具有分支的概率编程语言

• 发表时间: 2022
• 作者: Kazumasa Shimari;Takashi Ishio;Tetsuya Kanda;Katsuro Inoue;兼光 琢真
• 通讯作者: 兼光 琢真

機械学習によるループ不変条件の発見

使用机器学习寻找循环不变量

• 发表时间: 2021
• 作者: 森山直樹;天野友樹;清水貴弘;大島浩太;北川直哉;近藤 将成;関山 太朗
• 通讯作者: 関山 太朗

Gradual Typing for Extensibility by Rows

逐行扩展的渐进式打字

• 发表时间: 2020
• 作者: Taro Sekiyama;Atsushi Igarashi
• 通讯作者: Atsushi Igarashi