Research on software contracts for highly interoperable software modules

高度互操作软件模块的软件契约研究

• 批准号: 20H00582
• 负责人: 五十嵐 淳
• 金额: $ 28.45万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A)
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20H00582/
• 关键词: プログラミング言語; プログラム検証; 相互運用性; ソフトウェア契約; ソフトウエア契約

【研究項目1. モジュール間のデータ変換機構とその自動化の研究】前年度から行っているレコードとハッシュテーブルが相互運用な可能な言語の研究を進め，基本的な機能をSML#コンパイラ上に実装することができ，この成果について国内研究集会で論文発表を行った．一方で，SML#に実装されているOhoriの多相レコード計算の制限から再帰的データ構造の取り扱いに当初想定していなかった問題があること，ならびにコンパイラ内での中間処理に起因する制限から，ある種類のプログラムについてはうまくコンパイルできないことが判明した．前者について，解決の方策は既に得られているが理論的な問題がないことを確認する必要がある．後者については純粋にエンジニアリング的な問題であり時間をかければ解決可能であると見込んでいる．一般的なデータ変換の自動化機構については関連研究のサーベイなどを行った．また、関連して、LLVM IR からスマートコントラクト言語Michelsonへのコンパイル方式の研究を行った。これは多言語モジュールでスマートコントラクトを記述することにも繋がる。【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】交付申請書であげた(項目2-1)については，項目1のデータ変換自動化機構とも密接に関連することもあり，関連研究のサーベイに費した．(項目2-2)の多相型を持つ言語と動的型付言語間の相互運用を行うための実行検査については，前年度までの空間効率のよい実装の不可能性の理論的結果に基づき，不可能性がパラメータ性を実行時に保証するために使われている名前生成機構のみに因ることを理論的に示した．具体的には，空間効率の指標となるサイズ関数の定義を，連続したコアーションについてはサイズを定数と見做すことにすれば，空間効率がよいと見做せることを証明した．

[Project 1. Research on the Automation of the Inter-modal Switch Mechanism] In the previous year, the research on the inter-modal switch mechanism was carried out, and the basic functions of the switch mechanism were implemented. On the one hand, SML#is installed in the middle of Ohori's multi-phase circuit calculation limit, re-transmitted data structure selection, initial thinking, intermediate processing in the middle of the circuit, the cause of the limit, the type of circuit calculation limit, re-transmitted data structure, etc. The former is necessary to solve the problem of theory. The latter is a problem that can be solved in time. The general design of the automatic mechanism for the change of the relationship between the research and the service. Research on Michelson's Speech and Communication Methods This is the first time that I've ever been able to talk to you. [Project 2. Multi-language mobile communication system constitutes a system for the identification of mobile communication systems. Delivery of application forms (item 2-1). (Item 2-2) The spatial efficiency of polyphase speech and motion patterns is based on the theoretical results of impossibility theory. The impossibility theory is based on the theoretical results of impossibility theory. Specific space efficiency indicators such as the definition of the number, even if the number of fixed space efficiency.

项目成果

計算効果入門 ― プログラミングから理論まで ―

计算效应简介——从编程到理论——

• 发表时间: 2022
• 作者: 関山 太朗;勝股 審也;叢 悠悠
• 通讯作者: 叢 悠悠

Compilation of Coordinated Choice

协调选择汇编

• 发表时间: 2020
• 期刊: arXiv
• 作者: Yuki Nishida;Atsushi Igarashi
• 通讯作者: Atsushi Igarashi

代数的エフェクトとハンドラのためのエフェクトシステムの抽象化

代数效应和处理程序的效应系统抽象

• 发表时间: 2023
• 作者: 吉岡 拓真;関山 太朗;五十嵐 淳
• 通讯作者: 五十嵐 淳

Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus

依赖类型多阶段微积分的阶段感知相等类型

• 发表时间: 2022
• 期刊: 第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集
• 作者: Shuntaro Katsuda;Atsushi Igarashi
• 通讯作者: Atsushi Igarashi

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

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

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