2025/03/14 更新

写真a

クラ　サトシ
内藏　理史
所属
教育・総合科学学術院 教育学部
職名
講師（任期付）
学位
博士（情報学） ( 2022年03月 総合研究大学院大学 )
ホームページ
https://group-mmm.org/~skura/

経歴

  • 2024年04月
    -
    　

    早稲田大学   教育・総合科学学術院   講師（任期付き）

  • 2022年04月
    -
    2024年03月

    国立情報学研究所   アーキテクチャ科学研究系   特任研究員

  • 2022年04月
    -
    2024年03月

    University of Oxford   Department of Computer Science   Academic Visitor

  • 2022年04月
    -
    2024年03月

    独立行政法人日本学術振興会   海外特別研究員

  • 2021年04月
    -
    2022年03月

    独立行政法人日本学術振興会   特別研究員 DC2

学歴

  • 2019年04月
    -
    2022年03月

    総合研究大学院大学   複合科学研究科   情報学専攻  

  • 2017年04月
    -
    2019年03月

    東京大学   大学院情報理工学系研究科   コンピュータ科学専攻  

  • 2013年04月
    -
    2017年03月

    東京大学   理学部   情報科学科  

受賞

  • 優秀学生賞

    2021年09月   国立情報学研究所  

  • 日本ソフトウェア科学会第37回大会 優秀発表賞

    2020年09月   日本ソフトウェア科学会  

 

論文

▼全件表示

講演・口頭発表等

  • Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System

    Satoshi Kura, Hiroshi Unno

    The 29th ACM SIGPLAN International Conference on Functional Programming  

    発表年月： 2024年09月

    開催年月：
    2024年09月
    　
    　

  • Higher-Order Weakest Precondition Transformers via a CPS Transformation

    Satoshi Kura

    The 11th ACM SIGPLAN Workshop on Higher-Order Programming with Effects  

    発表年月： 2023年09月

  • Decision Tree Learning in CEGIS-Based Termination Analysis

    Satoshi Kura, Hiroshi Unno, Ichiro Hasuo

    33rd International Conference on Computer-Aided Verification  

    発表年月： 2021年07月

  • Graded Algebraic Theories

    Satoshi Kura

    23rd International Conference on Foundations of Software Science and Computation Structures  

    発表年月： 2021年03月

  • A Generic Semantic Construction of Dependent Refinement Type Systems, Categorically

    Satoshi Kura

    24th International Conference on Foundations of Software Science and Computation Structures  

    発表年月： 2021年03月

▼全件表示

共同研究・競争的資金等の研究課題

  • 述語変換子による合成性を活かした自動検証手法の圏論的意味論を経由した拡張

    日本学術振興会  科学研究費助成事業

    研究期間:

    2021年04月
    -
    2023年03月
     

    内藏 理史

    　概要を見る

    本年度は主にエフェクトハンドラーの検証のためのプログラム論理を圏論的意味論を用いて研究した．本研究のベースとなっているHermidaの研究ではfibrationと呼ばれるある種の関手に沿って単純型付きλ計算の意味論の"持ち上げ"を考えることでプログラムが満たす性質について議論するが，本研究ではエフェクトハンドラーの圏論的意味論として知られているEilenberg-Moore代数に対してある特定のfibrationに沿った持ち上げが存在するための十分条件を新たに与えた．さらに意味論側での持ち上げの存在の十分条件に対応するように構文側での十分条件を考えることで，エフェクトハンドラーの性質を証明するための推論規則を与えた．この推論規則は合成的であり，あるエフェクトハンドラーの性質の検証をそれぞれの代数的演算(algebraic operation)の性質の検証に帰着することができる．この推論規則を用いることでこれまで検証が難しかった，状態を扱うエフェクトハンドラーの検証が(現時点では非常に簡単なプログラムの例までしか考えていないものの)できるようになった．これらの研究成果は自身の博士論文の一つの章としてまとめた．また本研究成果の論文は近いうちに国際会議に投稿する予定である．

  • 圏論と自動検証による機械学習の仕様保証

    科学技術振興機構  戦略的な研究開発の推進 戦略的創造研究推進事業 ACT-X

    研究期間:

    2021年
    -
    2023年
     

    内藏 理史

    　概要を見る

    近年の機械学習の発展に伴い、機械学習のアルゴリズムに対してプライバシー・公平性・安全性など様々な要求が出てきています。確率的プログラムや微分可能プログラムとして書かれた機械学習のアルゴリズムの自動検証の新しい手法を、(1)プログラム論理や篩型システムなどの既存の自動検証を圏論的意味論を用いて一般化し、(2)確率的プログラムや微分可能プログラムに合わせた設定で具体化することで、手法の獲得を目指します。

 

現在担当している科目

▼全件表示

 

他学部・他研究科等兼任情報

  • 教育・総合科学学術院   大学院教育学研究科