安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論

用于安全可靠软件系统的高阶、类型和并发编程语言理论

基本信息

  • 批准号:
    20H04161
  • 负责人:
  • 金额:
    $ 11.32万
  • 依托单位:
  • 依托单位国家:
    日本
  • 项目类别:
    Grant-in-Aid for Scientific Research (B)
  • 财政年份:
    2020
  • 资助国家:
    日本
  • 起止时间:
    2020-04-01 至 2025-03-31
  • 项目状态:
    未结题

项目摘要

本研究の目的は以下のとおりであった。現代社会の基盤をなす科学技術である情報処理システム(いわゆる計算機プログラムを基礎とするが、それに限らず、より幅広い意味でのソフトウェアシステムを含む。)の安全性・信頼性ならびに生産性を高めるため、数理論理学に基づいてシステムを記述し正しさを検証するプログラミング言語理論を発展させ、狭義のプログラミング言語のみならず、より一般的な計算モデルにおける広義の「プログラム」としてのシステム記述に用いる。特に、最近の発展・普及が目覚ましい、高度な型システムや高階(higher-order)および並行(concurrent)・分散プログラムないしプログラミング言語に関する理論の研究を行う。当年度は以下を含む研究を研究協力者らとともに、他の研究とも連携して行なった。・構造化グラフの正規化の証明:関数的(functional)な表現が難しいとされるグラフ構造を関数的に表現する手法の一つであるOliveira-Cookの構造化グラフ(structured graph)において、表現(項)の冗長性を取り除くための正規化(normalization)の規則を定義・証明した。・複数参加者セッション型の一般プロセス型への変換:複数の参加者(プロセス)が通信を行う並行プロセス計算(concurrent process calculus)において、通信のプロトコル(順序等の手順)を表すセッション型(session type)から、プロセスの入出力の振る舞いを表すIgarashi-Kobayashiの一般型システム(generic type system, GTS)への変換を定義し、両者の関係を明らかにした。
The purpose of this study is to study the following problems. The foundation of modern society is science and technology, and information processing systems include computer science and technology. Safety, reliability, productivity, mathematical theory, basic theory, development of speech theory, narrow language theory, general calculation, definition of speech theory, description of speech theory In particular, recent developments in the field of speech and speech, high-order, concurrent, decentralized speech and speech theory are being studied. The following year, including the research collaborators, the research team and the research team. The proof of normalization of structured graph: the definition and proof of the rules of normalization of structured graph of Oliveira-Cook. The general change of the type of the plural participants: A plurality of participants communicate with each other and perform parallel computation.(concurrent process calculus), communication protocol (sequence, etc.)(session type), the input force, the vibration mode, the general type system (GTS), and the relationship between them are clearly defined.

项目成果

期刊论文数量(8)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
SMTソルバーを利用した算術式を含む高階関数の等価性検証手法
使用SMT求解器的算术表达式等高阶函数的等价验证方法
  • DOI:
  • 发表时间:
    2021
  • 期刊:
  • 影响因子:
    0
  • 作者:
    遠藤 瑛輔;住井 英二郎
  • 通讯作者:
    住井 英二郎
定理証明支援器Coqを用いた計算量の証明の改良
使用定理证明支持器 Coq 改进计算复杂性证明
  • DOI:
  • 发表时间:
    2021
  • 期刊:
  • 影响因子:
    0
  • 作者:
    中村 悠紀;住井 英二郎
  • 通讯作者:
    住井 英二郎
型システムを用いたロックフリースタックの検証
使用类型系统验证无锁堆栈
複数参加者非同期セッション型の一般プロセス型への変換
将多参与者异步会话类型转换为通用流程类型
  • DOI:
  • 发表时间:
    2023
  • 期刊:
  • 影响因子:
    0
  • 作者:
    細川 万里奈;住井 英二郎
  • 通讯作者:
    住井 英二郎
LEGO Education SPIKE PrimeのMicroPython環境における関数型リアクティブプログラミング
乐高教育 SPIKE Prime 的 MicroPython 环境中的函数式反应式编程
  • DOI:
  • 发表时间:
    2023
  • 期刊:
  • 影响因子:
    0
  • 作者:
    中里 匡亮;住井 英二郎
  • 通讯作者:
    住井 英二郎
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

住井 英二郎其他文献

Almost First-Class Language Embedding: Taming Staged Embedded DSLs
几乎一流的语言嵌入:驯服阶段式嵌入式 DSL
  • DOI:
    10.1145/2936314.2814217
  • 发表时间:
    2016
  • 期刊:
  • 影响因子:
    0
  • 作者:
    水野 雅之;住井 英二郎;合志清一;永原;Maximilian Scherr and Shigeru Chiba
  • 通讯作者:
    Maximilian Scherr and Shigeru Chiba
NetKAT with Cryptography
NetKAT 与密码学
  • DOI:
  • 发表时间:
    2019
  • 期刊:
  • 影响因子:
    0
  • 作者:
    菅原 慎之介;住井 英二郎
  • 通讯作者:
    住井 英二郎
spi計算における暗号プロトコルの形式的検証について
spi计算中密码协议的形式化验证
  • DOI:
  • 发表时间:
    2006
  • 期刊:
  • 影响因子:
    0
  • 作者:
    藤 尚稔;住井 英二郎;住井 英二郎
  • 通讯作者:
    住井 英二郎
4K カメラ用フォーカスアシストの開発
4K摄像机对焦辅助开发
  • DOI:
  • 发表时间:
    2017
  • 期刊:
  • 影响因子:
    0
  • 作者:
    遠藤 侑介;松本 宗太郎;上野 雄大;住井 英二郎;松本 行弘;T. Ikeda and M. Nagahara;M. Watanabe;合志清一
  • 通讯作者:
    合志清一
Evaluation of Heavy-Ion-Induced SEU Cross Sections of a 65 nm Thin BOX FD-SOI Flip-Flops Based on Stacked Inverter
基于堆叠逆变器的 65 nm 薄 BOX FD-SOI 触发器的重离子诱导 SEU 横截面评估
  • DOI:
  • 发表时间:
    2018
  • 期刊:
  • 影响因子:
    0
  • 作者:
    遠藤 侑介;松本 宗太郎;上野 雄大;住井 英二郎;松本 行弘;T. Ikeda and M. Nagahara;M. Watanabe;合志清一;山岡吉生;Jun Furuta
  • 通讯作者:
    Jun Furuta

住井 英二郎的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('住井 英二郎', 18)}}的其他基金

安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論
用于安全可靠软件系统的高阶、类型和并发编程语言理论
  • 批准号:
    23K20379
  • 财政年份:
    2024
  • 资助金额:
    $ 11.32万
  • 项目类别:
    Grant-in-Aid for Scientific Research (B)
プログラミング言語理論にもとづく広義情報処理システムセキュリティ
基于编程语言理论的广义信息处理系统安全
  • 批准号:
    22K19766
  • 财政年份:
    2022
  • 资助金额:
    $ 11.32万
  • 项目类别:
    Grant-in-Aid for Challenging Research (Exploratory)
先進的な型システムを備えた並列/分散プログラミング言語の設計と実装
具有高级类型系统的并行/分布式编程语言的设计和实现
  • 批准号:
    00J09726
  • 财政年份:
    2000
  • 资助金额:
    $ 11.32万
  • 项目类别:
    Grant-in-Aid for JSPS Fellows
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了