藤田研究室のホームページへようこそ!
藤田研究室では計算機支援による定理証明やモデル検査ツールを使った検証技術の研究をしています.

最新情報

1st January 2024
研究紹介--It's only a puzzle, but it is a puzzle after all--(HiKaLo シーズを見つけよう,北関東産学官研究会情報誌,2023)
1st April 2023
We are going to move to the new site ... under construction ... All Fools' Day! No, but this page here shall remain silent ...
15th February--17th Febuary 2023
Kyoto University RIMS Symposium "Group, Ring, Language and Related Areas in Computer Science",
Programme, 研究発表:K.Fujita, T.Kurata: 『Boolos' "The Hardest Logic Puzzle Ever" and Coinduction』
09 January 2023
合成的Z定理に関する論文(Z property for the shuffling calculus)が Mathematical Structures in Computer Science (Cambridge University Press) から出版, 2022/11/29 Accepted, Online DOI:10.1017/S0960129522000408
Z定理では困難であるが,合成的Z定理では証明可能である値呼び計算体系(The Shuffling Calculus)の合流性を示しました.従来手法では停止性とHindley-Rosenの補題から証明されていましたが,合成的Z定理を適用すると停止性から独立に証明可能となります.
2022/06/21--24
SAML2022: Symposium on Advances in Mathematical Logic 2022 チュートリアル : Introduction to the Curry-Howard isomorphism
京都大学 数理解析研究所RIMS 共同研究(公開型)「数理論理学とその応用」 :カリー・ハワード同型と証明の形式化
2022/03/25
数理パズルで楽しく学べる論理学を出版しました.身近なパズル,面白いパズル,最強のパズルに挑戦してみてください.
主題は,ゲーデルの完全性定理,カリー・ハワード同型の話題です.
ノート:2022年3月1日にバイデン米大統領は連邦議会で一般教書演説をしました.その時のネクタイの
2022/03/28--30
日本数学会2022年度年会 数学礎論 (埼玉大学)で研究発表
T.Kurata, K.Fujita: Spectral Spaces for Models of Intuitionistic Logic
2022/03/06--08
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) プログラム委員会委員
日本ソフトウェア科学会 プログラミング論研究会
2022/02/16--18
京都大学 数理解析研究所RIMS 共同研究 「論理・代数系・言語と計算機科学の周辺領域」 研究発表:
K.Fujita, T.Kurata: A general form on the logic puzzle of Boolos
2021/12/20--22
京都大学 数理解析研究所RIMS 共同研究 「証明論と計算の理論と応用」 赤坂陸来君(M1)が研究発表
R.Akasaka, K.Fujita. K.Nakazawa: 「合流性とZ定理について」
T.Kurata, K.Fujita: 「Spectral spaces for models of intuitionistic logic」
2021/09/14--17
日本数学会2021年度秋季総合分科会 数学礎論 (千葉大学)で研究発表
K.Fujita, T.Kurata: On formalization of logic puzzles a la George Boolos
2021/02/17--19
京都大学 数理解析研究所RIMS 共同研究Logic, Language, Algebraic System and Related Areas in Computer Science
研究発表:On formalization of logic puzzles a la Smullyan
January 2021
ラムダミュー計算の合流性に関する論文が Studia Logica (Springer Nature)から出版(Online: 20210121)
DOI 10.1007/s11225-020-09931-0
従来手法では困難でしたが, Z定理とよばれる定理を拡張して, divide-and-conquer的な新手法で合流性の 証明を与えることができました.
2020/09/22--25
日本数学会年会( 熊本大学)
2020/03/15--17
日本数学会年会(日本大学理工学部)で研究発表
2020/03/07--11
ラムダ計算と論理の早春セミナーで渡邊洋也君(B4)・富岡峻士君(M2)研究発表
2020/02/20--22
第52回 TRS Meeting で研究発表
January 2020
「計算の道」を表現する圏論的システムに関する論文が Theoretical Computer Science (Elsevier)から出版
DOI 10.1016/j.tcs.2020.01.002
並行計算と深く関係しています.計算のステップ数を数えたり, 隣接行列を使って計算の道の本数も数えることができます.
2019/12/24--26
京都大学 数理解析研究所 RIMS共同研究証明論とその周辺」:
富岡峻士君(M2) 研究発表 ラムダ計算の簡約グラフについて
2019/11/08
白鴎大学足利高校の研究室見学
October 2019
2階論理のモデルに関する論文が Fundamenta Informaticae (IOS Press) Volume 170 (1--3) から出版
DOI 10.3233/FI-2019-1861
可能世界モデル(位相的モデル)と代数的モデル(束論的モデル)の双対性に関する新しい結果で,高階の計算体系に応用できます.
2019/09/17--20
日本数学会2019年度秋季総合分科会(金沢大学)で研究発表:
Equational theory and reduction rules of reduction paths
2019/09/08
オープンキャンパス研究室見学
2019/04/18
理工学部しだれ記念会館
2019/04/13
赤城南面千本桃源郷
2019/04/11
恒例花見歓迎会 (桐生が岡公園)
2019/03/17--20
日本数学会2019年度年会(東京工業大学)で研究発表:
A Formal System of Reduction Paths for Parallel Reduction
2019/03/13
Professor Dr. Helmut Schwichtenberg (Ludwig-Maximilians-Universitat Munchen, Germany) 講演会:
Equality and extensionality
2019/03/08--11
ラムダ計算と論理の早春セミナー2019(草津セミナーハウス):
富岡峻士君(M1)と山野井涼華さん(B4)が研究発表
2019/03/06--08
第21回プログラミングおよびプログラミング言語ワークショップPPL2019(花巻市):
Z定理を用いたλμ計算の合流性証明
2019/02/21
卒業研究発表会
2019/01/23
HiKaLo シーズを見つけよう(2019)の研究紹介アップ
2019/01/01
2019年おめでとうございます!Webページも新しくなりました!
December 2018
チャーチ・ロッサーの定理に関する論文がInformation and Computation (Elsevier)から出版:
チャーチ・ロッサーの定理の新たな定量的証明方法です.DOI 10.1016/j.ic.2018.09.022 Open access
2018/09/25--27
研究会 49th TRS meeting伊香保で開催
2018/09/18--22
竹内外史追悼シンポジューム(神戸大学)
2018/08/30, 09/06
Swansea University (UK), Chalmers University of Technology (Sweden)で研究発表
2018/03/22--25
ラムダ計算と論理の早春セミナー2018(東京外語大・田沢湖研修施設)で研究発表
2018/03/18--21
日本数学会2018年度年会(東京大学)で研究発表:
The Church--Rosser Theorem and Quantitative Analysis of Witnesses
2018/03/05--09
JSPS Core-to-Core Program: 2nd Workshop on Mathematical Logic and Applications(金沢)で研究発表
2018/02/28
卒業研究発表会
2018/02/25--27
48th TRS meeting(仙台)で研究発表:The Church--Rosser theorem and analysis of reduction length
2018/01/17--18
Stochastic Models and their Applications (Osaka Univ.): Ty Ratanaさん(M2)が研究発表

研究室について

藤田研究室は2018年10月現在,藤田憲悦准教授,大学院博士課程前期1名,学部4年生5名, 学部3年1名(GFL)の計8名で構成されています.毎週2回各2時間程度のゼミを開き,メンバーが それぞれ学習したことについて発表します.

研究する分野は主に形式手法・検証技術(formal methods)です. システム設計上のミスの改善やプログラムの正しさを証明することでバグによる被害を抑えたり, 保守性・信頼性の向上につながる,現代において重要な立ち位置であるといえます.