東北大学大学院 情報科学研究科 情報基礎科学専攻 小林･住井研究室

This Page
Home

Main Contents

研究の概要

小林・住井研究室では，型システムなどの手法を利用したプログラム解析の研究を行っています．

近年，交通システム，医療機器，電子政府，電子商取引等，あらゆる社会基盤がコンピュータによって制御されつつあります．このような状況においては，ソフトウェアの欠陥が人命や財産の喪失という重大な事態を引き起こします．そこで，当研究室では，しっかりとした理論的土台に基づいたプログラミング言語処理系やプログラム検証ツールを構築することにより，正しく安全なソフトウェアの開発を支援することを目指しています．

新着情報

2014/05/01 お知らせ 住井准教授が教授に昇任しました．新しい研究室のWebサイトはこちらです．/ This Web page is obsolete. See the new laboratory's page instead.
2012/04/01 お知らせ 小林教授と松田助教の転出に伴い，小林・住井研究室は（亀山）・住井研究室となりました（東北大学電気・情報系における研究室名）．本Webサイトの内容は追って更新されます．現在の研究内容に関しては情報科学研究科の研究室紹介，学部生向け研究室紹介(PDF)などをご覧ください．
2013/05/13 お知らせ 研究室Webサーバが移転しました（URLは変わりません）。不具合等にお気づきの際は root ＠ kb.ecei.tohoku.ac.jp までお知らせください（法令に基づき、広告宣伝メールの送信はお断りします）。
2013/12/03 受賞 住井准教授が「先進的プログラミング言語理論の研究・開発と普及」によりソフトウエアジャパン2014にて2013年度ソフトウエアジャパンアワードを受賞することが決定しました．
2013/02/04 受賞 住井准教授が第9回（平成24年度）日本学術振興会賞を受賞しました．
2013/01/21 発表 D3の佐藤亮介君がPEPM 2013（部分評価とプログラム操作に関する国際ワークショップ）にて，論文"Towards a Scalable Software Model Checker for Higher-Order Programs"（海野広志博士，東京大学小林直樹教授との共著）に関する発表を行いました．
2012/10/27 発表 住井准教授がMicrosoft Research Asia Faculty Summit 2012（マイクロソフト研究所アジア 大学教員サミット）にて，"Activities and Experiences in the Young Academy of Japan"に関する発表を行いました．
2012/09/26 発表 D3の塚田君がIFIP TCS 2012（情報処理国際連合 理論計算機科学会議）にて，論文"An Intersection Type System for Deterministic Pushdown Automata"（東京大学小林直樹教授との共著）に関する発表を行いました．
2012/07/11 発表 D3の塚田君がICALP 2012（オートマトン，言語およびプログラミングに関する国際会議）にて，論文"Two-Level Game Semantics, Intersection Types and Recursion Schemes"（Oxford大学Luke Ong教授との共著）に関する発表を行いました．
2012/06/24 発表 住井准教授がLICS 2012（計算機科学における論理に関する国際会議）にて，論文"A Higher-Order Distributed Calculus with Name Creation"（元学生のアドリアン・ピエラール君との共著）に関する発表を行いました．
2012/06/05 受賞 D3の佐藤亮介君が情報処理学会論文賞を受賞しました．
2012/05/23 発表 M2の飛田君がFLOPS 2012（関数型・論理型プログラミングに関する国際会議）にて，論文"Exact Flow Analysis by Higher-Order Model Checking"（D3の塚田君，東京大学小林直樹教授との共著）に関する発表を行いました．
2012/04/14 受賞 住井准教授が船井学術賞を受賞しました．
2012/01/24 発表 小林教授がPEPM 2012（部分評価とプログラム操作に関する国際ワークショップ）にて，論文"Functional Programs as Compressed Data"（松田助教，篠原歩教授との共著）に関する発表を行いました．
2012/01/23 発表・受賞 松田助教がPEPM 2012（部分評価とプログラム操作に関する国際ワークショップ）にて，論文"Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals"（稲葉一浩博士，中野圭介准教授との共著，最優秀論文賞受賞）に関する発表を行いました．
2011/11/11 受賞 住井准教授が日本IBM科学賞を受賞しました．
2011/11/1 受賞 住井准教授がRIEC Award東北大学研究者賞を受賞しました．
2011/10/11 発表 小林教授がATVA 2011（検証と解析のための自動技術）にて，論文"Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols"（Morten Dahl博士，元学生の孫君，Hans Hüttel博士との共著）に関する発表を行いました．
2011/09/18 発表 小林教授がML Workshop 2011（関数型プログラミング言語「ML」に関する国際ワークショップ）にて，招待講演"Towards a software model checker for ML"を行いました．
2011/06/23 発表 小林教授がLICS 2011（計算機科学における論理に関する国際会議）にて，招待講演"Higher-Order Model Checking: From Theory to Practice"を行いました．
2011/06/09 受賞 小林教授が日本ソフトウェア科学会基礎研究賞を受賞しました．
2011/06/09 受賞 元学生の上嶋君と住井准教授が日本ソフトウェア科学会論文賞を受賞しました．
2011/06/07 発表 ポスドクの海野氏がPLDI 2011（プログラミング言語の設計と実装に関する国際会議）にて，論文"Predicate Abstraction and CEGAR for Higher-Order Model Checking"(小林教授，D2の佐藤亮介君との共著)に関する発表を行いました．
2011/03/29 発表 小林教授がFoSSaCS 2011（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes"に関する発表を行いました．
2011/03/28 発表 D3のAdrien Pierard君がFoSSaCS 2011（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"Sound Bisimulations for Higher-Order Distributed Process Calculus"(住井准教授との共著)に関する発表を行いました．
2011/02/28 講演会 国立情報学研究所の定兼邦彦氏をお招きして講演会を行いました．
2010/12/14 講演会 Aarhus UniversityのOlivier Danvy氏をお招きして講演会を行いました．
2010/12/03 講演会 Trinity College DublinのVasileious Koutavas氏をお招きして講演会を行いました．
2010/12/01 発表 ポスドクの海野氏がAPLAS 2010（プログラミング言語およびシステムに関するアジア会議）にて，論文"Verification of Tree-Processing Programs via Higher-Order Model Checking"に関する発表を行いました．
2010/10/21 講演会 CNRSのDavid Monniaux氏，Thomas Gawlitza氏をお招きして講演会を行いました．
2010/07/26 受賞 住井准教授がマイクロソフトリサーチ日本情報学研究賞を受賞しました．
2010/06/17 講演会 Institute of Cybernetics, Tallinn University of TechnologyのKeiko Nakata氏をお招きして講演会を行いました．
2010/03/26 発表 M2の塚田武志君がFoSSaCS 2010（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"Untyped Recursion Schemes and Infinite Intersection Types"に関する発表を行いました．
2010/01/22 発表 小林教授がPOPL 2010（プログラミング言語の原理に関する国際会議）にて，論文"Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification"に関する発表を行いました．
2010/01/20 発表 寺内助教がPOPL 2010（プログラミング言語の原理に関する国際会議）にて，論文"Dependent Types from Counterexamples"に関する発表を行いました．
2009/12/15 発表 住井准教授がAPLAS 2009（プログラミング言語およびシステムに関するアジア会議）にて，論文"The Higher-Order, Call-by-Value Applied Pi-Calculus"に関する発表を行いました．
2009/11/09 講演会 京都大学の四熊尚方氏をお招きして講演会を行いました．
2009/10/21 講演会 神戸大学の江口直日氏をお招きして講演会を行いました．
2009/09/15 講演会 東京大学の川本裕輔氏をお招きして講演会を行いました．
2009/09/09 発表 ポスドクの海野氏がPPDP 2009（宣言的プログラミングの原理と実践に関する国際会議）にて，論文"Dependent Type Inference with Interpolants"に関する発表を行いました．
2009/09/08 発表 住井准教授がCSL 2009（計算機科学論理学に関する欧州会議）にて，論文"A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References"に関する発表を行いました．
2009/09/07 発表 小林教授がPPDP 2009（宣言的プログラミングの原理と実践に関する国際会議）にて，論文"Model-Checking Higher-Order Functions"に関する発表を行いました．
2009/08/12 発表 小林教授がLICS 2009（計算機科学における論理に関する国際会議）にて，論文"A Type System Equivalent to Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes"に関する発表を行いました．
2009/08/10 発表 D1の安岡宏俊君がSAS 2009（静的解析に関する国際会議）にて，論文"Polymorphic Fractional Capabilities"に関する発表を行いました．
2009/07/22 講演会 東京大学の松田一孝氏をお招きして講演会を行いました．
2009/07/05 発表 小林教授がICALP 2009（オートマトン，言語およびプログラミングに関する国際会議）にて，論文"Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus"に関する発表を行いました．
2009/07/01 発表 M2の塚田武志君がTLCA 2009（型付ラムダ計算とその応用に関する国際会議）にて，論文"A Logical Foundation for Environment Classifiers"に関する発表を行いました．
2009/05/26 受賞 寺内助教が野口研究奨励賞を受賞しました．
2009/05/08 講演会 京都大学の五十嵐淳氏をお招きして講演会を行いました．
2009/03/26 発表 住井准教授がESOP 2009（プログラミングに関する欧州会議）にて，論文"A Theory of Non-Monotone Memory (Or: Contexts for free)"に関する発表を行いました．
2009/03/26 発表 M2の菊地大介君がESOP 2009（プログラミングに関する欧州会議）にて，論文"Type-Based Automated Verification of Authenticity in Cryptographic Protocols"に関する発表を行いました．
2009/03/24 講演会 国立情報学研究所のZhenjiang Hu氏をお招きして講演会を行いました．
2009/02/26 講演会 電気通信大学の中野圭介氏をお招きして講演会を行いました．
2009/01/30 受賞 小林教授が日本学術振興会賞を受賞することが決まりました．
2009/01/24 発表 M1の佐藤亮介君がPLAN-X 2009（XMLのためのプログラミング言語技法に関する国際ワークショップ）にて，論文"Ordered Types for Stream Processing of Tree-Structured Data"に関する発表を行いました．
2009/01/23 発表 小林教授がPOPL 2009（プログラミング言語の原理に関する国際会議）にて，論文"Types and higher-order recursion schemes for verification of higher-order programs"に関する発表を行いました．
2008/12/18 講演会 京都大学の照井一成氏をお招きして講演会を行いました．
2008/12/10 発表 ポスドクの末永君がAPLAS 2008（プログラミング言語およびシステムに関するアジア会議）にて，論文"Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References"に関する発表を行いました．
2008/11/21 講演会 国立情報学研究所の龍田真氏をお招きして講演会を行いました．
2008/10/21 講演会 京都大学の長谷川真人氏をお招きして講演会を行いました．
2008/10/15 講演会 東京大学の稲葉一浩氏をお招きして講演会を行いました．
2008/09/17 講演会 京都大学の蓮尾一郎氏をお招きして講演会を行いました．
2008/09/12 講演会 Coverity社のJohn Kodumal氏をお招きして講演会を行いました．
2008/08/06 講演会 MITの梅野真也氏をお招きして講演会を行いました．
2008/07/18 受賞 小林教授と大崎人士博士（産業総合技術研究所）による論文"Tree Automata for Non-Linear Arithmetic"が，RTA 2008（項書換えと応用に関する国際会議）にて，最優秀論文賞を受賞しました．
2008/07/10 発表 小林教授がCAV 2008（コンピュータ支援検証に関する国際会議）にて，論文"A Hybrid Type System for Lock-Freedom of Mobile Processes"に関する発表を行いました．
2008/06/25 発表 寺内助教がCSF 2008（コンピュータセキュリティの基礎に関する国際会議）にて，論文"A Type System for Observational Determinism"に関する発表を行いました．
2008/06/17 WEB ホームページを更新しました．
2008/06/13 講演会 京都大学の五十嵐淳氏をお招きして講演会を行いました．
2008/06/09 発表 寺内助教がPLDI 2008（プログラミング言語の設計と実装に関する国際会議）にて，論文"Checking Race Freedom via Linear Programming"に関する発表を行いました．
2008/05/30 受賞 元M2の須藤崇君と小林教授による論文「並行プログラミング言語へのチャネル使用法宣言の導入」が，平成19年度情報処理学会論文賞を受賞しました．
2008/04/19 受賞 住井准教授が「再帰的高階言語におけるプログラム等価性証明手法」に関する研究により，第7回船井情報科学奨励賞を受賞しました．
2008/04/16 発表 小林教授がFLOPS 2008（関数型・論理型プログラミングに関する国際会議）にて，招待講演"Substructural Type Systems for Program Analysis"を行いました．
2008/04/15 発表 D3（東京大学より指導委託）の海野君が，FLOPS 2008（関数型・論理型プログラミングに関する国際会議）にて，論文"On-Demand Refinement of Dependent Types"に関する発表を行いました．
2008/04/01 発表 寺内助教がESOP 2008（プログラミングに関する欧州会議）にて，論文"Inferring Channel Buffer Bounds via Linear Programming"に関する発表を行いました．
2008/04/01 発表 M2の金子君がESOP 2008（プログラミングに関する欧州会議）にて，論文"Linear Declassification"に関する発表を行いました．