- 実施方法
- オンライン・対面の両方で実施
- 説明会に並行して，学生によるQ&Aを開催
- オンライン
-
- 日程
- 9/25および9/26の9:35-10:20、11:15-12:00
- 会場
- Google Meet（大学のGoogleアカウントでご参加ください）
- 対面
-
- 日程
- 9/25および9/26の15:25〜16:10、17:05〜17:50
- 会場
- 電気情報システム・応物系3号館 108号室
「ちゃんと動く」ソフトウェア
現代では、パソコンや携帯電話は言うに及ばず、交通機関や電子政府、金融取引や医療機器など、社会の根幹や人命を左右するシステムがコンピュータにより制御されています。しかし、それらのコンピュータを実際に制御しているソフトウェアは、論理的・数理的な基礎の薄弱なまま、しばしば人的努力のみによって開発されていて、そのことが現実にさまざまな問題を引き起こす主因となっています。
本研究室では、このような問題に対処すべく、論理的・数理的基礎に基づいたソフトウェア開発のためのプログラミング言語・手法、ツール、計算モデル等に関する研究を行っています。以下は最近の研究テーマの例です。
プログラム等価性証明手法
二つのプログラムの振る舞いが等価であるか否かは、プログラムの最適化や検証にも密接に関連する、基本的かつ重要な問題です。私達は「環境双模倣」に基づくプログラム等価性証明手法を考案し、幅広いプログラミング言語および計算モデルに適用しました。
関数プログラミング
簡単・安全かつ強力なプログラミング手法・言語として近年になり再注目されている関数プログラミングおよび関数型言語に関し、トップレベルのプログラマ・技術者・研究者らと共に世界的に著名なプログラミングコンテストの主催を担当するなど、幅広い社会的活動を行っています。
双方向変換
ソフトウェア開発においては、変換とその「逆変換」の実装がしばしば要求されます。我々は「ちゃんと動く」双方向変換記述のためのプログラミング言語・手法を開発しています。
近年の卒論・修論テーマ
2023年度
- A Functional and Compositional Approach to Web Applications via Bidirectional Transformation （双方向変換に基づく関数的かつ合成的なウェブアプリケーション構成手法）
- インメモリデータベースにおけるレコード選択演算のSIMD利用による最適化
- 完全なストリーム融合によるソフトウェア無線
- Rust への Fractional Ownership の動的検査の導入
- 双方向変換言語におけるpin演算子の有用性の確認
- OCamlにおけるEmbedding by Unembedding
- 配列言語によるモルフォロジー画像処理の実装
- ベクトル加算の性能計測とコード生成時最適化
- プログラム検証器Stainlessによる関数型プログラムの等価性検証
2022年度
- 構造化グラフの正規化の証明の修正
- 複数参加者非同期セッション型の一般プロセス型への変換
- LEGO Education SPIKE PrimeのMicroPython環境における関数型リアクティブプログラミング
- An Arrow Metalanguage for Partially Invertible Computation （部分可逆計算のためのアローメタ言語）
- Analyses of Quantified/Negated Relative Clauses with Polynomial Event Semantics （多項イベント意味論による量化/否定関係節の分析）
さらに過去の卒論・修論テーマ
2021年度
- MetaOCamlのCコード生成機能を用いたサッカーロボット用ルールベース言語の設計と実装
- データベースクエリにおけるBoolean selectionのコード生成
- Completeなストリーム融合によるソフトウェア無線のディジタル信号処理
- Haskellによる関数的なTensorFlowの検討
- Polymorphic Gradual Typing and Structure Editor Calculus for Programs with Holes （ホールのあるプログラムのための多相的漸進的型付けと構造エディタ計算）
- Type-Based Verification of Deadlock- and Livelock-Freedom of Treiber’s Stack （型システムを用いたTreiberのスタックのデッドロックフリー性およびライブロックフリー性の検証）
2020年度
- MetaOCamlによる自律型ロボットのためのＣコード生成
- 定理証明支援器Coqを用いた計算量の証明の改良
- Textual Entailment with Polynomial Event Semantics（多項式イベント意味論によるテキスト推論：繋辞文と全称量化）
- 画像処理における関数プログラミングの利点の欠点：HIPとOpenCVの比較を通じた検討
- 順方向プログラムと逆方向動作例からのwell-behavedな双方向プログラムの合成
- SMTソルバーを利用した算術式を含む高階関数の等価性検証手法
2019年度
- Coroutine Pipelineの高速化
- Polymorphic gradual typing with holes
- Arduino機器制御のための相対モナドに基づく埋め込み領域特化言語
- 型システムを用いたロックフリースタックの検証
- セキュリティ型付き λ 計算の環境双模倣の検証と改良
- 並行性・非決定性・状態・暗号を備えた NetKAT
- 範疇文法の代数的な埋め込み手法
- 関数型と和型を持つ可逆プログラミング言語
2018年度
- F*による高階関数の等価性の証明
- UnCALの純粋関数型並列実装
- ブロックチェーン合意形成プロトコルのCoqによる証明からのコード抽出
- MetaOCaml による高水準表現からのGPU カーネルコード生成
- Linear Quipper: 埋め込み線形型付き量子プログラミング言語
- FUnCAL の記述性の評価: UnQL+ の糖衣構文に関するケーススタディ
2017年度
- 分数型と負型を持つ線形型付き高階関数型可逆プログラミング言語の並行プログラムによる実装
- 確率的プログラミング言語Hakaru10による隠れマルコフモデル問題への取り組み
- メモリ使用量比較のための環境双模倣の拡張
- NetKAT with Cryptography（暗号プリミティブを追加したNetKAT）
- 情報流解析のための環境双模倣
- 必要呼び意味論と名前呼び意味論の対応の形式的検証
- ロックフリーアルゴリズムの形式的検証
- コード生成計算<NJ>にカリーハワード対応する論理体系の構築
2016年度
- MetaOCamlによるGPGPUプログラミング
- 等価性が双模倣に基づくグラフに対する関数プログラミング
- ロボット制御プログラム生成のための関数型DSL
- 軽量マークアップ言語処理系の帰納的プログラミングによるカスタマイズ
- 並べ替え・外部結合・グループ化を含むデータベースクエリのプログラミング言語への統合
- 非限定継続を扱えるラムダ計算における文脈等価性のための健全かつ完全な双模倣
2015年度
- MinCamlのK正規化の形式的検証
- データ構造の低水準操作に関する分離論理を用いた定理証明
- セキュリティ型付きラムダ計算のための環境双模倣
- CamlNetKat: ソフトウェア・デファインド・ネットワークのための型付き埋め込みDSL
- 機械学習による関数型ブーリアンプログラムの型推論
- 多相関数のインライン展開による特殊化に関する研究
- Up-to context techniqueを用いた環境双模倣の準判定器
住井・松田研の研究生活
下記の他に授業期間中は週1でゼミを行っています。主な内容は研究調査の発表などです。
B4
- 4月
- 配属，歓迎会（お花見）
- 4月〜
- 教科書を輪読
- 7月
- オープンキャンパス
- 10月
- 卒論テーマ決定・芋煮会
- 1月
- 卒論提出
- 2月
- 卒論発表会（中野研・海野研と合同）
M1
- 7月
- オープンキャンパス
- 10月
- 芋煮会
M2
- 7月
- オープンキャンパス
- 10月
- 芋煮会
- 12月
- 修論予備審査
- 2月
- 修論提出・審査
- 3月
- 歓送会
僕らと一緒にソフトウェアを科学しよう！
さらなる情報は住井・松田研ウェブサイトへ