差分
このページの2つのバージョン間の差分を表示します。
| 両方とも前のリビジョン 前のリビジョン 次のリビジョン | 前のリビジョン | ||
| start [2019/10/09 19:45] – [メンバー] ksk | start [2019/10/21 15:08] (現在) – 削除 nishiyama | ||
|---|---|---|---|
| 行 1: | 行 1: | ||
| - | ~~Title: 中野研究室 ~~ | ||
| - | |||
| - | 東北大学電気通信研究所 コンピューティング情報理論研究室 | ||
| - | ====== 中野研究室 ====== | ||
| - | |||
| - | 中野研究室では，プログラミングに関連するさまざまな研究を行っています．\\ | ||
| - | 主に以下のようなトピックを研究テーマとしています． | ||
| - | |||
| - | ==== プログラミング言語処理系 ==== | ||
| - | |||
| - | 「プログラミング言語」と言われて皆さんがイメージするのはどのような言語でしょう？ C, Java, それとも他の言語でしょうか． 世の中には何千ものプログラミング言語が存在すると言われています． こんなにたくさんの言語が存在する理由は， 目的や用途によって適した言語が異なるためです． プログラミング言語処理系の研究では， 従来のプログラミング言語に手を加えて目的に適した機能を追加したり， 用途に合った小さなプログラミング言語を自ら開発したりすることを実現しています． 既存のコンパイラの修正による実行プログラムの高速化にも取り組んでいます． | ||
| - | |||
| - | ==== 関数型プログラミング ==== | ||
| - | |||
| - | 近年，関数型プログラミングとよばれるデータフローを明確にした プログラミングスタイルが話題となっています． 複数のビジネス誌に特集として取り上げられるなど， 企業からの注目も高い研究分野です． 実際，Google の検索エンジンで利用されていることで有名な MapReduce は 関数型プログラミングのアイデアから生まれたものであり， 膨大なメッセージの効率的な処理が必要な Twitter の実装も Scala という言語を用いて関数型プログラミングによって実現されています． 関数型プログラミングについての研究では， より使いやすくするための解決方法を提案したり， 実行効率を向上させるための新たな実装を開発したりしています． | ||
| - | |||
| - | ==== プログラム検証 ==== | ||
| - | |||
| - | 皆さんは，講義や演習でプログラミングをするとき， 正しく動作することをどのように確認しているでしょうか． いろいろな入力でテスト実行してみたり， プログラムの途中に print 命令を挿入して途中経過を観察したりしていませんか？ プログラムの検証は， 「実行せずにプログラムの性質を知る」ための研究です． 基本的にテスト実行では限られた数の入力しかテストできないため， 本当に正しく動くかは保証されません． 本研究では，全ての入力に対して正しく動作するということを数学的な手法で証明しているため， より正確にプログラムの性質を知ることが可能になります． | ||
| - | |||
| - | ==== プログラム変換 ==== | ||
| - | |||
| - | 一般的に「短絡的に書いたプログラムは，読みやすい一方で効率が悪く， 効率を良くするために工夫して書いたプログラムは， 読みにくい上にデバッグもしにくい」というジレンマがあります． 効率を意識したプログラムは，複雑なアルゴリズムを用いているため， ちょっとした問題設定の変更に対してどのように修正すべきかは単純ではありません． プログラム変換の研究では， 短絡的に書いたプログラムを 効率のよいプログラムに自動変換することを実現します． これにより，読みやすく修正もしやすいプログラミングのもとで， 効率の良い実行プログラムを得ることができます． | ||
| - | |||
| - | ==== 形式言語理論 ==== | ||
| - | |||
| - | 講義などでオートマトンや形式文法などを勉強したことがあると思いますが， 形式言語理論はそれらを深く探求する分野です． 講義では何のために役に立つか分からないまま学習していたかもしれませんが， プログラミング言語の分野では非常に重要なテーマです． ここで挙げている研究テーマの中では最も理論的で数学的な素養が必要になりますが， プログラムの検証から効率化にいたるまで， さまざまなプログラミングの分野で応用可能な実用的な研究の1つです． | ||
| - | |||
| - | ==== 双方向変換 ==== | ||
| - | |||
| - | 双方向変換系は，データベースを安全かつ効率的に更新するための研究です． データベースから必要な情報だけを抽出して見やすく整形したものをビューとよびますが， このビューの内容を修正することで， その修正をデータベース側に反映してしまおうというのが双方向変換のアイデアです． ここで「必要な情報を抽出して見やすく整形する」 という部分を一つのプログラムで記述されていると考えると， そのプログラムは， データベースを入力としてビューを出力するものであると見なせます． したがって，ビュー側の修正をデータベースに反映するためには， このプログラムを逆方向に実行する必要があるわけです． 双方向変換の研究では， この逆方向の実行を自動化するための枠組みを対象にして， 実現するための理論やその実用化に取り組んでいます． | ||
| - | |||
| - | ==== プログラミング言語意味論 ==== | ||
| - | |||
| - | プログラミング言語意味論は主に表示的意味論・操作的意味論・公理的意味論からなっています． | ||
| - | 表示的意味論はプログラミング言語の構成要素（型やプログラムなど）を数学的構造（ある種の空間や関数など，あるいは別の言語）に「表示（解釈）」し，プログラミング言語の構造や性質を数学的に解明します． | ||
| - | 操作的意味論はプログラムの手続き的な意味を定めるもので，この操作的意味論と表示的意味論の一致を示すことで，両意味論の正当性を高めます． | ||
| - | 公理的意味論はプログラムのための論理体系を構築し，プログラムに関する推論を形式的に行う手段を提供します． | ||
| - | これら意味論は各種定理により互いに関係を持ち，一体となって研究されます． | ||
| - | その主な応用として，「プログラミング言語の設計」と「プログラミング言語の検証体系・推論体系の開発」の2つが挙げられます． | ||
| - | プログラミング言語意味論は，上記に挙げられた研究室の各テーマの基礎理論としても重要です． | ||
| - | |||
| - | ===== メンバー ===== | ||
| - | |||
| - | ^ 役職 | ||
| - | | 教授 | ||
| - | | 助教 | ||
| - | | 特別研究学生 | 西山 舜 | NISHIYAMA Shun | snishiya + @riec.tohoku.ac.jp | ||
| - | | 修士課程 | ||
| - | | 学部 | ||
| - | | ::: | 眞田 耕太 | ||
| - | |||
| - | OB： | ||
| - | * 2019年：阿部 和敬，小澤 祐也，高橋 祐多 | ||
| - | ===== リンク ===== | ||
| - | * [[https:// | ||
| - | * [[http:// | ||
| - | * [[https:// | ||
| - | * [[http:// | ||
| - | * [[http:// | ||
| - | * [[internal: | ||