Basic Information

Faculty

• 工学部 工学部 情報学科

Professional Memberships

• 日本ソフトウェア科学会
• ACM

Academic Degree

• (The University of Tokyo)
• (The University of Tokyo)

Academic Resume (Graduate Schools)

• The University of Tokyo, 大学院理学系研究科情報科学専攻博士課程, 修了
• The University of Tokyo, 大学院理学系研究科情報科学専攻修士課程, 修了

Academic Resume (Undergraduate School/Majors)

• The University of Tokyo, 理学部情報科学科, 卒業

Research History

• From Apr. 2023, To Mar. 2026

  Kyoto University, Graduate School of Informatics, Dean
• From Oct. 2012, To Present

  Kyoto University, Graduate School of Informatics, 教授
• From Apr. 2007, To Sep. 2012

  Kyoto University, Graduate School of Informatics, 准教授
• From Apr. 2006, To Apr. 2007

  Kyoto University, Graduate School of Informatics, 助教授
• From Apr. 2002, To Apr. 2006

  Kyoto University, Graduate School of Informatics, 講師
• From Apr. 2000, To Apr. 2002

  The University of Tokyo, Graduate School of Arts and Sciences, 助手

Profile

• Profile

  ソフトウェアのバグを少なくするための理論の研究を、ソフトウェアを記述するためのプログラミング言語の観点から行っています。特に、プログラム中の誤りをプログラムを実行することなく発見できる枠組みである型理論に興味があります。

Language of Instruction

• English

ID,URL

• ORCID ID

  0000-0002-5143-9764

• J-Global ID

  200901018941019247

• External link

  http://kaken.nii.ac.jp/ja/r/40323456

Website(s) (URL(s))

• http://www.fos.kuis.kyoto-u.ac.jp/~igarashi

researchmap URL

• https://researchmap.jp/Atsushi.Igarashi

Research

Research Topics, Overview of the research

• Research Topics

  Principles of Programming Languages, Type Theory

Research Interests

• プログラミング言語の基礎理論
• 漸進的型付け
• 型理論
• マルチステージプログラミング
• オブジェクト指向
• ソフトウェア
• 型システム

Research Areas

• Informatics, Information theory
• Informatics, Software

Papers

• Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types

  Takashi Suwa; Atsushi Igarashi

  Proceedings of ECOOP 2026, Jun. 2026, Peer-reviewed

  
• Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  Proceedings of ECOOP 2026, Jun. 2026, Peer-reviewed

  
• Contextual Metaprogramming for Session Types

  Pedro Ângelo; Atsushi Igarashi; Yuito Murase; Vasco T. Vasconcelos

  Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I., 10 Apr. 2026, Peer-reviewed

  
• An ML-style module system for cross-stage type abstraction in multi-stage programming

  Takashi Suwa; Atsushi Igarashi

  Science of Computer Programming, Mar. 2026, Peer-reviewed

  
• 動的型推論を備えた空間効率の良い漸進的型付け

  大志万優生; 関山太朗; 五十嵐淳

  日本ソフトウェア科学会第42回大会論文集, Sep. 2025

  
• Unifying Function- and Argument-First Bidirectional Type Systems

  Takuma Yoshioka and Taro Sekiyama and Atsushi Igarashi

  日本ソフトウェア科学会第42回大会論文集, Sep. 2025

  
• Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops

  Sewon Park; Atsushi Igarashi

  Proceedings of Formal Methods in Computer-Aided Design (FMCAD), Oct. 2025, Peer-reviewed

  
• Contextual Metaprogramming for Session Types

  Pedro Ângelo; Atsushi Igarashi; Yuito Murase; Vasco Vasconcelos

  第27回プログラミングおよびプログラミング言語ワークショップ(PPL2025)論文集, Mar. 2025, Peer-reviewed

  
• Type-Based Verification of Connectivity Constraints in Lattice Surgery

  Ryo Wakizaka; Yasunari Suzuki; Atsushi Igarashi

  Proceedings of the 22nd Asian Symposium on Programming Languages and Systems, 28 Oct. 2024, Peer-reviewed

  
• Rabbit: A Language to Model and Verify Data Flow in Networked Systems

  Terunobu Inaba; Yutaka Ishikawa; Atsushi Igarashi; Taro Sekiyama

  2024 International Symposium on Networks, Computers and Communications (ISNCC), 22 Oct. 2024, Peer-reviewed

  Access this paper :

  
• Signature restriction for polymorphic algebraic effects

  TARO SEKIYAMA; TAKESHI TSUKADA; ATSUSHI IGARASHI

  Journal of Functional Programming, 27 May 2024, Peer-reviewed

  
• Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

  Atsushi Igarashi; Shota Ozaki; Taro Sekiyama; Yudai Tanabe

  Proceedings of the ACM on Programming Languages, 20 Jun. 2024, Peer-reviewed

  
• An ML-Style Module System for Cross-Stage Type Abstraction in Multi-stage Programming

  Takashi Suwa; Atsushi Igarashi

  Proceedings of Intl. Symposium on Functional and Logic Programming, May 2024, Peer-reviewed

  
• Linear Contextual Metaprogramming and Session Types

  Pedro Ângelo; Atsushi Igarashi; Vasco T. Vasconcelos

  Electronic Proceedings in Theoretical Computer Science, 06 Apr. 2024, Peer-reviewed

  
• 命令型プログラムの安全性検証のための所有権主導変換

  小林亮太; 中村烈士; 五十嵐淳; 末永幸平; 小林直樹

  第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集, Mar. 2024, Peer-reviewed

  
• iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns

  Yuki Nishida; Kohei Suenaga; Atsushi Igarashi

  Proceedings of 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024, Peer-reviewed

  
• Rabbit: a modeling language for verifying cybersecurity in IoT system

  Terunobu Inaba; Yutaka Ishikawa; Atsushi Igarashi; Taro Sekiyama

  第145回情報処理学会プログラミング研究会資料, Aug. 2023

  
• LLTZ: LLMV IR からスマートコントラクト記述言語 Michelson へのコンパイラ

  臼澤嘉; 末永幸平; 古瀬淳; 五十嵐淳

  第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集, Mar. 2023, Peer-reviewed, Last author

  
• Contextual Modal Type Theory with Polymorphic Contexts

  Yuito Murase; Yuichi Nishiwaki; Atsushi Igarashi

  Proceedings of European Symposium on Programming, Apr. 2023, Peer-reviewed, Last author

  Access this paper :

  
• HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types.

  Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  CoRR, 2021

  
• Verification of a Merkle Patricia Tree Library Using F.

  Sota Sato; Ryotaro Banno; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  CoRR, 2021

  
• Compilation of Coordinated Choice.

  Yuki Nishida 0001; Atsushi Igarashi

  CoRR, 2020

  
• Signature restriction for polymorphic algebraic effects.

  Taro Sekiyama; Takeshi Tsukada; Atsushi Igarashi

  Proc. ACM Program. Lang., 2020

  
• Manifest Contracts with Intersection Types.

  Yuki Nishida 0001; Atsushi Igarashi

  CoRR, 2019

  
• Reasoning about Polymorphic Manifest Contracts.

  Taro Sekiyama; Atsushi Igarashi

  CoRR, 2018

  
• Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq

  奥村 健太郎; 五十嵐 淳

  日本ソフトウェア科学会大会論文集, 07 Sep. 2014

  
• Visibility of Context-oriented Behavior and State in L

  Hirschfeld Robert; 増原 英彦; 五十嵐 淳

  日本ソフトウェア科学会大会論文集, 07 Sep. 2014

  
• SCameleer: スマートコントラクト記述言語SCamlのための自動検証器

  服部 佑哉; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会第39回大会論文集, Sep. 2022

  
• スマートコントラクト検証器Helmholtzのためのエラー原因提示手法

  小野 雄登; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会第39回大会論文集, Sep. 2022

  
• 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法

  梅木 孝輔; 関山 太朗; 五十嵐 淳

  日本ソフトウェア科学会第39回大会論文集, Sep. 2022

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

  Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  New Generation Computing, Jul. 2022, Peer-reviewed

  Access this paper :

  
• ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて

  竹房 あつ子; 五十嵐 淳; 関山 太朗; 松井 俊浩; 小野 泰司; 福田 健介; 蓮尾 一郎; 合田 憲人; 石川 裕

  第154回情報処理学会システムソフトウェアとオペレーティング・システム研究会資料, May 2022

  
• Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus

  Shuntaro Katsuda; Atsushi Igarashi

  第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, Mar. 2022, Peer-reviewed

  
• Type-based Qubit Allocation for a First-Order Quantum Programming Language

  Ryo Wakizawa; Atsushi Igarashi

  第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集, Mar. 2022, Peer-reviewed

  
• Is Space-Efficient Polymorphic Gradual Typing Possible?

  Shota Ozaki; Taro Sekiyama; Atsushi Igarashi

  Informal Proceedings of Scheme and Functional Programming Workshop, Sep. 2021, Peer-reviewed

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

  Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  Tools and Algorithms for the Construction and Analysis of Systems, TACAS2021, Mar. 2021, Peer-reviewed

  Access this paper :

  
• Space-Efficient Gradual Typing in Coercion-Passing Style.

  Yuya Tsuda; Atsushi Igarashi; Tomoya Tabuchi

  34th European Conference on Object-Oriented Programming, ECOOP 2020, Nov. 2020, Peer-reviewed

  
• 量子ビット連結性制約検査のための依存型システム

  脇坂 遼; 五十嵐 淳

  日本ソフトウェア科学会第37回大会論文集, Sep. 2020

  
• Signature restriction for polymorphic algebraic effects

  Taro Sekiyama; Takeshi Tsukada; Atsushi Igarashi

  Proceedings of the ACM on Programming Languages, 02 Aug. 2020, Peer-reviewed

  
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

  John Toman; Ren Siqi; Kohei Suenaga; Atsushi Igarashi; Naoki Kobayashi

  Programming Languages and Systems, Apr. 2020, Peer-reviewed

  Access this paper :

  
• スタック領域上での時間的メモリ安全性を保証する静的解析手法

  矢杉 和義; 五十嵐 淳

  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, Mar. 2020, Peer-reviewed

  
• スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証

  齋藤 大聖; 西田 雄気; 五十嵐 淳; 末永 幸平

  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, Mar. 2020, Peer-reviewed

  
• F* を用いた Merkle Patricia Tree ライブラリの形式検証

  佐藤 聡太; 古瀬 淳; 末永 幸平; 五十嵐 淳

  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)論文集, Mar. 2020, Peer-reviewed

  
• Space-Efficient Gradual Typing in Coercion-Passing Style

  Yuya Tsuda; Atsushi Igarashi; Tomoya Tabuchi

  Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), Jan. 2020, Peer-reviewed

  
• Gradual Typing for Extensibility by Rows

  Taro Sekiyama; Atsushi Igarashi

  Informal Proceedings of the 1st International Workshop on Gradual Typing (WGT2020), Jan. 2020, Peer-reviewed

  
• A Dependently Typed Multi-stage Calculus.

  Akira Kawata; Atsushi Igarashi

  Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, Nov. 2019, Peer-reviewed

  Access this paper :

  
• Manifest Contracts with Intersection Types.

  Yuki Nishida; Atsushi Igarashi

  Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, Nov. 2019, Peer-reviewed

  Access this paper :

  
• Temporal Verification of Programs via First-Order Fixpoint Logic.

  Naoki Kobayashi; Takeshi Nishikawa; Atsushi Igarashi; Hiroshi Unno

  Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, Oct. 2019, Peer-reviewed

  
• A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping

  Hiroaki Inoue; Atsushi Igarashi

  Science of Computer Programming, Jun. 2019, Peer-reviewed

  Access this paper :

  
• Handling Polymorphic Algebraic Effects

  Taro Sekiyama; Atsushi Igarashi

  Proceedings of European Symposium on Programming (ESOP2019), Apr. 2019, Peer-reviewed

  
• 空間効率の良いコアーション計算のためのコアーション渡し形式

  津田優也; 五十嵐淳

  第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, Mar. 2019, Peer-reviewed

  
• Gradual session types

  ATSUSHI IGARASHI; PETER THIEMANN; YUYA TSUDA; VASCO T. VASCONCELOS; PHILIP WADLER

  Journal of Functional Programming, 2019, Peer-reviewed

  
• Dynamic Type Inference for Gradual Hindley-Milner Typing

  Yusuke Miyazaki; Taro Sekiyama; Atsushi Igarashi

  Proceedings of the ACM on Programming Languages, Jan. 2019, Peer-reviewed

  
• Nondetermnistic Manifest Contracts

  Yuki Nishida; Atsushi Igarashi

  Proceedings of theInternational Symposium on Principles and Practice of Declarative Programming, Sep. 2018, Peer-reviewed

  
• ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions

  Hiroaki Inoue; Tomoyuki Aotani; Atsushi Igarashi

  Proceedings of the 32nd European Conference on Object-Oriented Programming, Jul. 2018, Peer-reviewed

  
• Method Safety Mechanism for Asynchronous Layer Deactivation

  Tetsuo Kamina; Tomoyuki Aotani; Hidehiko Masuhara; Atsushi Igarashi

  Science of Computer Programming, Mar. 2018, Peer-reviewed

  
• Automated Verification of Functional Correctness of Race-Free GPU Programs

  Kensuke Kojima; Akifumi Imanishi; Atsushi Igarashi

  Journal of Automated Reasoning, Mar. 2018, Peer-reviewed

  
• A Guess-and-Assume Approach to Loop Fusion for Program Verification

  Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi

  Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Jan. 2018, Peer-reviewed

  
• A Nonstandard Functional Programming Language

  Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2017), Nov. 2017, Peer-reviewed

  
• A DSL for Compensable and Interruptible Executions

  Hiroaki Inoue; Tomoyuki Aotani; Atsushi Igarashi

  Proceedings of 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), Oct. 2017, Peer-reviewed

  
• C言語における無効なスタック領域へのポインタを検出する静的解析

  矢杉 和義; 五十嵐 淳

  日本ソフトウェア科学会第34回大会論文集, Sep. 2017

  
• On Polymorphic Gradual Typing

  Yuu Igarashi; Taro Sekiyama; Atsushi Igarashi

  Proceedings of the ACM on Programming Languages, Sep. 2017, Peer-reviewed

  
• Gradual Session Types

  Atsushi Igarashi; Peter Thiemann; Vasco T; Vasconcelos; Philip Wadler

  Proceedings of the ACM on Programming Languages, Sep. 2017, Peer-reviewed

  
• A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations

  Yusuke Miyazaki; Atsushi Igarashi

  第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, Mar. 2017, Peer-reviewed

  
• A Hoare logic for GPU Kernels

  Kensuke Kojima; Atsushi Igarashi

  ACM Transactions on Computational Logic, 01 Feb. 2017, Peer-reviewed

  
• Stateful manifest contracts

  Taro Sekiyama; Atsushi Igarashi

  Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 01 Jan. 2017, Peer-reviewed

  
• Verification of Code Generators via Higher-Order Model Checking

  Takashi Suwa; Takeshi Tsukada; Naoki Kobayashi; Atsushi Igarashi

  Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'17), Jan. 2017, Peer-reviewed

  
• Polymorphic Manifest Contracts, Revised and Resolved

  Taro Sekiyama; Atsushi Igarashi; Michael Greenberg

  ACM Transactions on Programming Languages and Systems, Jan. 2017, Peer-reviewed

  
• Automated Verification of Functional Correctness of Race-Free GPU Programs

  Kensuke Kojima; Akifumi Imanishi; Atsushi Igarashi

  Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Nov. 2016, Peer-reviewed

  
• 階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール

  馬谷 誠二; 藤原 康史; 五十嵐 淳

  日本ソフトウェア科学会第33回大会論文集, Sep. 2016

  
• An Extended Behavioral Type System for Memory-Leak Freedom

  Qi Tan; Kohei Suenaga; Atsushi Igarashi

  日本ソフトウェア科学会第33回大会論文集, Sep. 2016

  
• SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証

  奥村 健太郎; 小島 健介; 五十嵐 淳

  第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, Mar. 2016, Peer-reviewed

  
• Gradual typing for delimited continuations

  Yusuke Miyazaki; Taro Sekiyama; Atsushi Igarashi

  The 5th Script To Program Evolution Workshop, 2016, Peer-reviewed

  
• A Library-Based Approach to Context-Dependent Computation with Reactive Values

  Hiroaki Inoue; Atsushi Igarashi

  Proceedings of Constrained and Reactive Objects Workshop (CROW2016), 2016, Peer-reviewed

  
• 参照を備えた多段階計算のための多相的型システム

  小林 恵; 五十嵐淳

  日本ソフトウェア科学会第32回大会論文集, Sep. 2015

  
• Visibility of Context-oriented Behavior and State in L

  Robert Hirschfeld; Hidehiko Masuhara; Atsushi Igarashi; Tim Felgentreff

  Computer Software, Aug. 2015, Peer-reviewed

  Access this paper :

  
• Method Safety Mechanism for Asynchronous Layer Deactivation

  Tetsuo Kamina; Tomoyuki Aotani; Hidehiko Masuhara; Atsushi Igarashi

  International Workshop on Context-Oriented Programming, COP'15 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'15, Jul. 2015, Peer-reviewed

  
• Manifest contracts for datatypes

  Taro Sekiyama; Yuki Nishida; Atsushi Igarashi

  Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 14 Jan. 2015, Peer-reviewed

  
• A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers

  Hiroaki Inoue; Atsushi Igarashi

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015, Peer-reviewed

  
• Shifting the Blame: A Blame Calculus with Delimited Control

  Taro Sekiyama; Soichiro Ueda; Atsushi Igarashi

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015, Peer-reviewed

  
• Automatic Memory Management Based on Program Transformation using Ownerships

  Tatsuya Sonobe; Kohei Suenaga; Atsushi Igarashi

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), Nov. 2014, Peer-reviewed

  
• Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse

  Minoru Kinoshita; Kohei Suenaga; Atsushi Igarashi

  Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Sep. 2014, Peer-reviewed

  
• On-Demand Layer Activation for Type-Safe Deactivation

  Tetsuo Kamina; Tomoyuki Aotani; Atsushi Igarashi

  International Workshop on Context-Oriented Programming, COP'14 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, Jul. 2014, Peer-reviewed

  
• Towards Type-Safe JCop: A type system for layer inheritance and first-class layers

  Hiroaki Inoue; Atsushi Igarashi; Malte Appeltauer; Robert Hirschfeldi

  International Workshop on Context-Oriented Programming, COP'12 - Co-located with the 26th European Conference on Object-Oriented Programming, ECOOP'14, Jul. 2014, Peer-reviewed

  
• On Cross-Stage Persistence in Multi-Stage Programming

  Yuichiro Hanada; Atsushi Igarashi

  Proceedings of Intl. Symposium on Functional and Logic Programming (FLOPS2014), Jun. 2014, Peer-reviewed

  
• 顕在的契約計算のための代数的データ型

  関山 太朗; 西田 雄気; 五十嵐 淳

  第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 2014, Peer-reviewed

  
• A Hoare Logic for SIMT Programs

  Kensuke Kojima; Atsushi Igarashi

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2013), Dec. 2013, Peer-reviewed

  
• 多段階計算λ▹のための越段階埋込

  花田 裕一朗; 五十嵐 淳

  日本ソフトウェア科学会第30回大会論文集, Sep. 2013

  
• Layer Refinement in L

  Robert Hirschfeld; Atsushi Igarashi; Hidehiko Masuhara

  並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), Aug. 2013

  
• Matching MyType to subtyping

  Chieri Saito; Atsushi Igarashi

  Science of Computer Programming, Jul. 2013, Peer-reviewed

  
• L: Context-oriented programming with only layers

  Robert Hirschfeld; Hidehiko Masuhara; Atsushi Igarashi

  Proceedings of the 5th International Workshop on Context-Oriented Programming, COP 2013, Jul. 2013, Peer-reviewed

  
• Model-Checking Higher-Order Programs with Recursive Types

  Naoki Kobayashi; Atsushi Igarashi

  Proceedings of European Symposium on Programming (ESOP2013), 2013, Peer-reviewed

  
• Type-based safe resource deallocation for shared-memory concurrency

  Kohei Suenaga; Ryota Fukuda; Atsushi Igarashi

  Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Oct. 2012, Peer-reviewed

  
• A Type System for Dynamic Layer Composition

  Atsushi Igarashi; Robert Hirschfeld; Hidehiko Masuhara

  Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), Oct. 2012, Peer-reviewed

  
• 顕在的契約計算におけるアップキャスト除去

  関山 太朗; 五十嵐 淳

  第14回プログラミングおよびプログラミング言語ワークショップ, 2012, Peer-reviewed

  
• Constructive linear-time temporal logic: Proof systems and Kripke semantics

  Kensuke Kojima; Atsushi Igarashi

  Information and Computation, Dec. 2011, Peer-reviewed

  
• Systematic Derivation of a λ○ Virtual Machine with Low-Level Code Generation by using Fusion Transformation

  小山内 幸一; 五十嵐 淳

  日本ソフトウェア科学会第28回大会論文集, Sep. 2011

  
• Polymorphic Contracts

  Joao Filipe Belo; Michael Greenberg; Atsushi Igarashi; Benjamin C. Pierce

  Proceedings of European Symposium on Programming (ESOP2011), Mar. 2011, Peer-reviewed

  
• Special track on object-oriented languages and systems

  D. Ancona; S. Chiba; A. Igarashi; A. Kellens

  Proceedings of the ACM Symposium on Applied Computing, 2011, Peer-reviewed

  
• Gradual typing for generics

  Lintaro Ina; Atsushi Igarashi

  Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, 2011, Peer-reviewed

  
• ContextFJ: A minimal core calculus for context-oriented programming

  Robert Hirschfeld; Atsushi Igarashi; Hidehiko Masuhara

  Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages, FOAL 2011, 2011, Peer-reviewed

  
• A Logical Foundation for Environment Classifiers

  Takeshi Tsukada; Atsushi Igarashi

  Logical Methods in Computer Science, 18 Dec. 2010, Peer-reviewed

  
• Mostly modular compilation of crosscutting concerns by contextual predicate dispatch

  Shigeru Chiba; Atsushi Igarashi; Salikh Zakirov

  Proceedings of Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Oct. 2010, Peer-reviewed

  
• Type relaxed weaving

  H. Masuhara; A. Igarashi; M. Toyama

  AOSD.10 - 9th International Conference on Aspect-Oriented Software Development, 2010, Peer-reviewed

  
• A Logical Foundation for Environment Classifiers

  Takeshi Tsukada; Atsushi Igarashi

  Proceedings of Typed Lambda Calculi and Applications (TLCA2009), Jun. 2009, Peer-reviewed

  
• Gradual Typing for Featherweight Java

  INA Lintaro; IGARASHI Atsushi

  Computer Software, Apr. 2009, Peer-reviewed

  
• Matching ThisType to subtyping

  Chieri Saito; Atsushi Igarashi

  Proceedings of the ACM Symposium on Applied Computing, 2009, Peer-reviewed

  
• Self type constructors

  Chieri Saito; Atsushi Igarashi

  Proceeding of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA 09, 2009, Peer-reviewed

  
• Towards gradual typing for generics

  Lintaro Ina; Atsushi Igarashi

  Proceedings for the 1st Workshop on Script to Program Evolution, STOP'09 in Conjunction with European Conference on Object-Oriented Programming, ECOOP'09, 2009, Peer-reviewed

  
• Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

  Naokata Shikuma; Atsushi Igarashi

  Logical Methods in Computer Science, 20 Sep. 2008, Peer-reviewed

  
• On Constructive Linear-Time Temporal Logic

  Kensuke Kojima; Atsushi Igarashi

  Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), Jun. 2008

  
• Lightweight family polymorphism

  Chieri Saito; Atsushi Igarashi; Mirko Viroli

  Journal of Functional Programming, May 2008, Peer-reviewed

  
• Featherweight Java のための漸進的型付け

  伊奈 林太郎; 五十嵐 淳

  第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, Mar. 2008, Peer-reviewed

  
• 文脈依存資源使用解析のための型システム

  仲井間 達也; 五十嵐 淳; 小林 直樹

  第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)論文集, Mar. 2008, Peer-reviewed

  
• Calculi of meta-variables

  M. Sato; T. Sakurai; Y. Kameyama; A. Igarashi

  Frontiers of Computer Science in China, 2008, Peer-reviewed

  
• The essence of lightweight family polymorphism

  Chieri Saito; Atsushi Igarashi

  Journal of Object Technology, 2008, Peer-reviewed

  
• Proving Noninterference by a Fully Complete Translation to the Simply Typed λ-Calculus

  Naokata Shikuma; Atsushi Igarashi

  Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, Dec. 2007

  
• Variant path types for scalable extensibility

  Atsushi Igarashi; Mirko Viroli

  Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA '07, Oct. 2007, Peer-reviewed

  
• The Essence of Lightweight Family Polymorphism

  Chieri Saito; Atsushi Igarashi

  Proceedings of 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), Jul. 2007, Peer-reviewed

  
• An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification

  IWAMA FUTOSHI; IGARASHI ATSUSHI; KOBAYASHI NAOKI

  情報処理学会論文誌. プログラミング, 15 Mar. 2007, Peer-reviewed

  
• Union types for object-oriented programming

  A. Igarashi; H. Nagira

  Journal of Object Technology, 2007, Peer-reviewed

  
• Variant Path Types for Scalable Extensibility

  Atsushi Igarashi; Mirko Viroli

  Proceedings of International Workshop on Foundations and Developments of Object-Oriented Languages, Jan. 2007, Peer-reviewed

  
• Deriving compilers and virtual machines for a multi-level language

  Atsushi Igarashi; Masashi Iwaki

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2007), 2007, Peer-reviewed

  
• Variant parametric types: A flexible subtyping scheme for generics

  Atsushi Igarashi; Mirko Viroli

  ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Sep. 2006, Peer-reviewed

  
• 様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明

  四熊 尚方; 五十嵐 淳

  第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)論文集, Mar. 2006, Peer-reviewed

  
• Resource usage analysis for a functional language with exceptions

  F. Iwama; A. Igarashi; N. Kobayashi

  Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 2006, Peer-reviewed

  
• A modal type system for multi-level generating extensions with persistent code

  Y. Yuse; A. Igarashi

  PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006, Peer-reviewed

  
• Union types for object-oriented programming

  A. Igarashi; H. Nagira

  Proceedings of the ACM Symposium on Applied Computing, 2006, Peer-reviewed

  
• Resource usage analysis

  A Igarashi; N Kobayashi

  ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Mar. 2005, Peer-reviewed

  
• 例外機構を備えた言語のための資源使用法解析

  岩間 太; 五十嵐 淳; 小林 直樹

  第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, Mar. 2005, Peer-reviewed

  
• メタプログラミングのための時相論理に基づく型付λ計算

  湯瀬 芳洋; 五十嵐 淳

  第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集, Mar. 2005, Peer-reviewed

  
• Lightweight family polymorphism

  A Igarashi; C Saito; M Viroli

  Proceedings of Asian Symposium on Programming Languages and Systems (APLAS2005), 2005, Peer-reviewed

  
• Generics・Union 型を導入したオブジェクト指向計算体系

  柳楽 秀士; 五十嵐 淳

  第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)論文集, Mar. 2004, Peer-reviewed

  
• A generic type system for the Pi-calculus

  A Igarashi; N Kobayashi

  THEORETICAL COMPUTER SCIENCE, Jan. 2004, Peer-reviewed

  
• A modal foundation for secure information flow

  Kenji Miyamoto; Atsushi Igarashi

  Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication,187-203, 2004, Peer-reviewed

  
• Union 型を導入したオブジェクト指向計算体系

  柳楽 秀士; 五十嵐 淳

  日本ソフトウェア科学会第20回大会論文集, Sep. 2003, Peer-reviewed

  
• 擬似引用を持つ型付計算体系λq

  山本 和樹; 岡本 暁広; 五十嵐 淳; 佐藤 雅彦

  第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, Mar. 2003, Peer-reviewed

  
• Calculi of meta-variables

  M Sato; T Sakurai; Y Kameyama; A Igarashi

  COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2003, Peer-reviewed

  
• On Inner Classes

  Atsushi Igarashi; Benjamin C. Pierce

  Information and Computation, Aug. 2002, Peer-reviewed

  
• Foundations for Virtual Types

  Atsushi Igarashi; Benjamin C. Pierce

  Information and Computation, May 2002, Peer-reviewed

  
• Resource usage analysis

  Atsushi Igarashi; Naoki Kobayashi

  Proceedings of Principles of Programming Languages (POPL02), Jan. 2002, Peer-reviewed

  
• On variance-based subtyping for parametric types

  A Igarashi; M Viroli

  ECOOP 2002 - OBJECT-ORIENTED PROGRAMMING, 2002, Peer-reviewed

  
• Featherweight Java: A minimal core calculus for Java and GJ

  A Igarashi; BC Pierce; P Wadler

  ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, May 2001, Peer-reviewed

  
• A Recipe for Raw Types

  Atsushi Igarashi; Benjamin C. Pierce; Philip Wadler

  Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL8), Jan. 2001, Peer-reviewed

  
• A generic type system for the Pi-calculus

  A. Igarashi; N. Kobayashi

  Conference Record of the Annual ACM Symposium on Principles of Programming Languages, Jan. 2001, Peer-reviewed

  
• Garbage Collection Based on a Linear Type System

  Atsushi Igarashi; Naoki Kobayashi

  Proceedings of the 3rd ACM SIGPLAN Wokshop on Types in Compilation (TIC'00), Sep. 2000, Peer-reviewed

  
• Type reconstruction for linear pi-calculus with I/O subtyping

  A Igarashi; N Kobayashi

  INFORMATION AND COMPUTATION, Aug. 2000, Peer-reviewed

  
• On inner classes

  A Igarashi; BC Pierce

  ECOOP 2000 - OBJECT-ORIENTED PROGRAMMING, Jun. 2000, Peer-reviewed

  
• On Inner Classes

  Atsushi Igarashi; Benjamin C. Pierce

  Informal Proceedings of International Workshop on Foundations of Object-Oriented Languages (FOOL7), Jan. 2000, Peer-reviewed

  
• Featherweight Java - A minimal core calculus for Java and GJ

  A Igarashi; B Pierce; P Wadler

  Proceedings of ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), Oct. 1999, Peer-reviewed

  
• Foundations for virtual types

  A Igarashi; BC Pierce

  Proceedings of European Conference on Object-Oriented Programming (ECOOP'99), Jun. 1999, Peer-reviewed

  
• Foundations for Virtual Types

  Atsushi Igarashi; Benjamin C. Pierce

  Informal Proceedings of International Workshop on Foundations of Object-Oriented Languages (FOOL6), Jan. 1999, Peer-reviewed

  
• Type-based Analysis of Communication for Concurrent Programming Languages

  Atsushi Igarashi; Naoki Kobayashi

  Proceedings of the Fourth International Static Analysis Symposium, Sep. 1997, Peer-reviewed

  

Misc.

• Functional and logic programming: Selected papers of FLOPS 2022

  Michael Hanus; Atsushi Igarashi

  Science of Computer Programming, Dec. 2024

  
• Preface to the JOT special issue on ECOOP 2021: selected workshop papers.

  Davide Ancona; Olivier Flückiger; Adrian Francalanza; Robert Hirschfeld; Atsushi Igarashi; Yu David Liu; Hidehiko Masuhara; Chris Seaton; Harumi Watanabe

  Journal of Object Technology, 2022

  
• 日本ソフトウェア科学会第31回大会報告

  五十嵐淳

  コンピュータソフトウェア, Feb. 2015, Invited

  
• 京都大学 Teen Racketeer 養成コース

  五十嵐 淳; 中澤 巧爾; 馬谷 誠二; 関山 太朗; 花田 裕一朗; 大元 武; 宮本 洋平; 末永 幸平

  第17回プログラミングおよびプログラミング言語ワークショップ, 2015

  
• 今熱い! 快進撃のOCaml

  五十嵐淳; Jacques Garrigue; 古瀬 淳

  ソフトウェアデザイン, Jan. 2014, Invited

  
• Logical relations for a manifest calculus, fixed

  Taro Sekiyama; Atsushi Igarashi

  The 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects, 2012, Peer-reviewed

  
• Formal Techniques for Java-Like Programs Report on the 10th Workshop FTfJP at ECOOP 2008

  Elvira Albert; Anindya Banerjee; Sophia Drossopoulou; Marieke Huisman; Atsushi Igarashi; Gary T. Leavens; Peter Mueller; Tobias Wrigstad

  OBJECT-ORIENTED TECHNOLOGY, 2009, Peer-reviewed

  
• Editorial message: Special track on object oriented programming languages and systems

  D. Ancona; R. Raje; M. Viroli; U. Bellur; V. Bono; J. Boyland; G. Castagna; A. Coglio; P. Cointe; P. Costanza; S. Drossopoulou; E. Ernst; G. Fox; J. Gray; A. Igarashi; R. Klefstad; D. Lea; M. Parashar; G. Rimassa; V. Sassone; Y. Smaragdakis; D. Syme; B. Tekinerdogan; J. Vitek; E. Zucca

  Proceedings of the ACM Symposium on Applied Computing, 2005, Peer-reviewed

  
• Generic Java: Safety and Reusability by Polymorphic Typing in Object-Oriented Programming

  IGARASHI Atsushi

  IPSJ Magazine, 15 Jun. 2004

  
• TACS 2001およびManfred Paul賞授賞式

  五十嵐 淳; 住井 英二郎

  情報処理, 05 Feb. 2002

  
• 『正しい』ソフトウェアの構築法 - 型システムとその応用

  五十嵐 淳

  京都大学大学院情報学研究科 第5 回情報学シンポジウム 「情報社会の基盤を拓くソフトウェア研究」 平成12 年12 月10 日（火曜日） 「『正しい』ソフトウェアの構築法 - 型システムとその応用」 五十嵐 淳 氏（京都大学情報学研究科）, 2000

  

Presentations

• 漸進的型付き多相ラムダ計算

  五十嵐 雄; 関山 太朗; 五十嵐 淳

  第19回プログラミングおよびプログラミング言語ワークショップ, 2017

  
• 限定継続演算子 shift/reset のための漸進的型付け

  宮崎 勇輔; 関山 太朗; 五十嵐 淳

  第18回プログラミングおよびプログラミング言語ワークショップ, 2016

  
• (I Can't Get No) Verification

  Atsushi Igarashi

  The 2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, Dec. 2022, Invited

  
• Dependently-Typed Multi-Stage Programming Revisited

  Atsushi Igarashi

  ACM SIGPLAN 2020 Workshop on Partial Evaluation and Program Manipulation (PEPM), Jan. 2020, Invited

  
• Type Systems for Dynamic Layer Composition

  Atsushi Igarashi

  International Workshop on Foundations of Aspect-Oriented Languages, Mar. 2013, Invited

  
• トップカンファレンスに論文を通す方法

  日本ソフトウェア科学会第29回大会, Sep. 2012, 日本ソフトウェア科学会

  
• Featherweight Approach to FOOL

  European Conference on Object-Oriented Programming, Jul. 2011, AITO

  
• Towards Pactical Resource Usage Analysis

  プログラム解析ワークショップ, Aug. 2007, 日本IBM東京基礎研究所

  
• Processes as Types: A Generic Framework of Behavioral Type Systems

  The 4th International Workshop on Foundations of Coordination Languages and Service Architectures, Aug. 2005

  

Books and Other Publications

• n月刊ラムダノート Vol.6, No.1

  五十嵐淳, Contributor, #3 計算を抽象的に捉える ― タグレスファイナル法によるアプローチ（五十嵐淳）

  ラムダノート, Jan. 2026

  Find Kyoto University's collection of books :

  
• Proceedings of the 15th ACM International Workshop on Context-Oriented Programming and Advanced Modularity

  Atsushi Igarashi

  ACM Press, 17 Jul. 2023

  Find Kyoto University's collection of books :

  
• COP 2022: International Workshop on Context-Oriented Programming and Advanced Modularity (collocated with ECOOP)

  Atsushi Igarashi

  ACM Press, 07 Jun. 2022

  Find Kyoto University's collection of books :

  
• Functional and Logic Programming: Proceedings of the 16th International Symposium, FLOPS 2022, Kyoto, Japan, May 2022

  Michael Hanus; Atsushi Igarashi, Joint editor

  Springer, Apr. 2022

  Find Kyoto University's collection of books :

  
• Encyclopedia of theoretical computer science

  徳山, 豪; 小林, 直樹; 岩間, 一雄; 渡辺, 治; 今井, 浩; 南出, 靖彦; 五十嵐, 淳; 長谷川, 真人, Joint editor

  朝倉書店, Jan. 2022

  Find Kyoto University's collection of books :

  
• Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

  Manuel Hermenegildo; Atsushi Igarashi, Editor

  The ACM Press, Jan. 2019, Not refereed

  
• Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016. Proceedings

  Atsushi Igarashi, Editor

  Springer-Verlag, Nov. 2016, Not refereed

  
• Concurrent Objects and Beyond: Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday

  Gul Agha; Atsushi Igarashi; Naoki Kobayashi; Hidehiko Masuhara; Satoshi Matsuoka; Etsuya Shibayama; Kenjiro Taura, Joint editor

  Springer-Verlag, 2014, Not refereed

  
• Programming Languages and Systems: Proceedings of the 10th Asian Symposium, APLAS 2012

  Ranjit Jhala; Atsushi Igarashi, Joint editor

  Springer-Verlag, Dec. 2012, Not refereed

  
• プログラミング言語の基礎概念

  五十嵐 淳

  サイエンス社, Jul. 2011, Not refereed

  Find Kyoto University's collection of books :

  
• プログラミング in OCaml ～関数型プログラミングの基礎からGUI構築まで～

  五十嵐 淳

  技術評論社, 30 Nov. 2007, Not refereed

  Find Kyoto University's collection of books :

  

Industrial Property Rights

• 特願2017-246154, プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム

  末永 幸平; 今西 諒文; 五十嵐 淳

  

Awards

• 12 Sep. 2024

  日本ソフトウェア科学会フェロー
• 12 Sep. 2024

  日本ソフトウェア科学会フェロー
• Nov. 2006

  日本アイ・ビー・エム, 第20回日本IBM科学賞(コンピュータサイエンス分野)
• Nov. 2009

  マイクロソフト株式会社, 第1回マイクロソフトリサーチ日本情報学研究賞(基礎的情報学分野)
• Apr. 2009

  文部科学省, 科学技術分野の文部科学大臣表彰 若手科学者賞
• Jul. 2011

  AITO, Dahl-Nygaard Junior Prize
• Sep. 2015

  日本ソフトウェア科学会, 日本ソフトウェア科学会高橋奨励賞
• Sep. 2020

  日本ソフトウェア科学会, 日本ソフトウェア科学会基礎研究賞
• 14 Apr. 2021

  文部科学省, 科学技術分野の文部科学大臣表彰 科学技術賞研究部門
• Jun. 2019

  日本学術振興会, 平成30年度特別研究員等審査会専門委員(書面担当)の表彰

External funds: Kakenhi

• 高信頼ソフトウェアコード生成システムのためのプログラミング言語基盤

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  五十嵐 淳

  From 01 Apr. 2026, To 31 Mar. 2030, Adopted

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-26H02493/
• Program Verification Techniques for the AI Era

  Grant-in-Aid for Scientific Research (S)

  Broad Section J

  The University of Tokyo

  小林 直樹

  From 31 Aug. 2020, To 31 Mar. 2025, Granted

  プログラム検証;高階モデル検査;高階不動点論理;機械学習;不動点論理

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20H05703/
• Research on software contracts for highly interoperable software modules

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  五十嵐 淳

  From 01 Apr. 2020, To 31 Mar. 2025, Granted

  プログラミング言語;プログラム検証;相互運用性;ソフトウェア契約;ソフトウエア契約

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20H00582/
• Program Verification Based on Higher-Order Fixpoint Logic

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  The University of Tokyo

  小林 直樹

  From 01 Apr. 2020, To 31 Mar. 2021, Discontinued

  プログラム検証;高階不動点論理;確率付き高階不動点論理;モデル検査;高階モデル検査

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20H00577/
• Enhancement of Formal Verification for IoT Systems

  Grant-in-Aid for Scientific Research (B)

  Basic Section 60050:Software-related

  Kyoto University

  Kohei Suenaga

  From 01 Apr. 2019, To 31 Mar. 2024, Project Closed

  ハイブリッドシステム;モデル検査;プログラム検証;形式検証;ブラックボックス検査;モニタリング;PDR;IoT;強化学習;機械学習;形式手法

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19H04084/
• Deepening of a self-extendable software verification system based on class theory

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Masahiko Sato

  From 01 Apr. 2017, To 31 Mar. 2021, Project Closed

  クラス理論;型理論;証明検証;ソフトウェアの安全性;仕様記述・検証;証明支援系

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17H01724/
• Theory of Gradual Typing for Modern Programming Languages

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Igarashi Atsushi

  From 01 Apr. 2017, To 31 Mar. 2021, Project Closed

  漸進的型付け;プログラミング言語;型システム;計算効果;顕在的契約計算;非決定計算;トレース意味論

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17H01723/
• Refinement and Extension of Higher-Order Model Checking

  Grant-in-Aid for Scientific Research (S)

  The University of Tokyo

  Naoki Kobayashi

  From 29 May 2015, To 31 Mar. 2020, Project Closed

  高階モデル検査;プログラム検証;データ圧縮;型システム;関数型プログラム;高階不動点論理;不動点論理;高階文法;確率付き文法;高階論理;共通型

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15H05706/
• Construction of a self-extendable software verification system based on class theory

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Masahiko Sato

  From 01 Apr. 2013, To 31 Mar. 2017, Project Closed

  クラス理論;型理論;証明検証;ソフトウェアの安全性;仕様記述・検証;証明支援系

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280025/
• Theory of Higher-Order Typed Programs based Software Contracts

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Atsushi Igarashi

  From 01 Apr. 2013, To 31 Mar. 2017, Project Closed

  プログラミング言語;ソフトウェア契約;計算効果;プログラム検証;トレース意味論;代入;限定継続;ゲーム意味論;shift/reset

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280024/
• Study on Highly Reliable Programming Languages for Code Generation

  Grant-in-Aid for Scientific Research (B)

  University of Tsukuba

  YUKIYOSHI KAMEYAMA

  From 01 Apr. 2013, To 31 Mar. 2016, Project Closed

  ディペンダブルコンピューティング;関数型プログラム言語;プログラム生成;プログラム検証;プログラム変換;プログラム特化;高性能計算;型システム;関数型プログラミング言語;実行時プログラム生成;プログラミング言語;ソフトウェア検証

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280020/
• Higher-Order Model Checking and its Applications

  Grant-in-Aid for Scientific Research (S)

  The University of Tokyo;Tohoku University

  Naoki Kobayashi

  From 31 May 2011, To 31 Mar. 2016, Project Closed

  高階モデル検査;プログラム検証;データ圧縮;高階文法;型システム;関数型プログラム;関数型言語;高階再帰スキーム;型理論

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23220001/
• New development of research on bug-free software construction environment

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Masahiko SATO

  From 01 Apr. 2010, To 31 Mar. 2013, Project Closed

  ソフトウェア検証;クラス理論;ソフトウェアの安全性;型理論;項書換;自然枠組;ソフトウェア開発;メタ言語;メタ理論;式の理論;抽象操作

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22300008/
• A Study on modularization mechanisms to integrate hierarchical and crosscutting decomposition for the post-aspect era

  Grant-in-Aid for Scientific Research (A)

  The University of Tokyo;Tokyo Institute of Technology

  Shigeru CHIBA

  From 01 Apr. 2010, To 31 Mar. 2015, Project Closed

  ソフトウェア・モジュール化;オブジェクト指向;アスペクト指向;文脈指向;ソフトウェア開発効率化・安定化;ソフトウェア学;プログラミング言語;モジュール化;型システム

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22240002/
• Theory and Design of a Safe and Flexible Programming Language Based On the Integration of Static and Dynamic Typing

  Grant-in-Aid for Young Scientists (A)

  Kyoto University

  Atsushi IGARASHI

  From 01 Apr. 2009, To 31 Mar. 2013, Project Closed

  オブジェクト指向言語;漸進的型付け;プログラミング言語;Java 言語;ジェネリクス;型安全性;コントラクト;Java言語;ソフトウェア契約;ソフトウェア・コントラクト

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21680002/
• Expanding Aspect-Oriented Programming

  Grant-in-Aid for Scientific Research (B)

  The University of Tokyo

  Hidehiko MASUHARA

  From 01 Apr. 2009, To 31 Mar. 2013, Project Closed

  横断的関心事;アスペクト指向;文脈指向;セキュリティ;意味論;型安全性;プログラミング言語;モジュール性;最適化;アスペクト指向プログラミング;セキュリティーポリシー;イベント駆動;文脈指向プログラミング;モジュール化;EventCJ;ContextJ;セキュリティポリシー;AspectJ;分散ソフトウェア

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21300006/
• Foundation of Programming Languages for Code Generation

  Grant-in-Aid for Scientific Research (B)

  University of Tsukuba

  Yukiyoshi KAMEYAMA

  From 01 Apr. 2009, To 31 Mar. 2013, Project Closed

  プログラミング言語論;プログラミングパラダイム;プログラム言語論;プログラム生成;型システム;高信頼ソフトウェア;プログラムの論理;コード生成;マルチステージプログラミング;様相論理;コントールオペレータ;型推論;多相型;融合変換;コントロールオペレータ;型エラー;Curry-Howardの対応

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21300005/
• Advancement and Application of Type Theory for Improving Software Safety

  Grant-in-Aid for Scientific Research (A)

  Tohoku University

  Naoki KOBAYASHI

  From 01 Apr. 2008, To 31 Mar. 2011, Project Closed

  ソフトウェア検証;型システム;高階モデル検査;資源使用法検証;プログラム解析;型理論;述語抽象化;メモリ使用法解析;モデル検査;高階再帰スキーム;資源使用法解析;ツリーオートマトン

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20240001/
• Software development environment based on integration of computation and logic

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Masahiko SATO

  From 01 Apr. 2007, To 31 Mar. 2010, Project Closed

  自然枠組;ソフトウェア開発;ソフトウェア検証;メタ言語;式の理論;メタ理論;抽象操作;メタ変数

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19300007/
• Study on Type Theory to Promote Software Reuse

  Grant-in-Aid for Young Scientists (B)

  Kyoto University

  Atsushi IGARASHI

  From 01 Apr. 2006, To 31 Mar. 2009, Project Closed

  プログラム言語論;オブジェクト指向;型システム;ソフトウェア;安全性;オブジェクト指向言語;再利用性;軽量族多相;漸進的型付け;ユニオン型

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18700026/
• Aspect-Oriented Software Development Methodology for Enhancing Productivity and Safety

  Grant-in-Aid for Scientific Research (A)

  The University of Tokyo

  Tetsuo TAMAI

  From 01 Apr. 2006, To 31 Mar. 2010, Project Closed

  アスペクト指向プログラミング;セキュリティ;ソフトウェア工学;ディスペンダブル・コンピューティング;UML;形式手法;ソフトウェア開発効率化・安定化;要求工学;ディスペンタブル・コンピューティング;プログラム言語;ディペンダブル・コンピューティング;ディスペンダブル、コンピューティング;ソフトウェア開発効率化、安定化

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18200001/
• 安全・安心な環境適応型ソフトウェアの基礎理論に関する研究

  Grant-in-Aid for Scientific Research on Priority Areas

  Science and Engineering

  Kyoto University

  五十嵐 淳

  From 01 Apr. 2006, To 31 Mar. 2007, Project Closed

  環境適応型ソフトウェア;線形時間時相論理;型理論;明示的環境;限定継続

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18049044/
• Type Theory for Software Safety

  Grant-in-Aid for Scientific Research (B)

  Tohoku University

  Naoki KOBAYSHI

  From 01 Apr. 2005, To 31 Mar. 2008, Project Closed

  プログラム検証;プログラム解析;型理論;関数型プログラム;並行プログラム;情報流解析;型システム;デッドロック;資源使用法解析;プログラム等価性;線形最適化問題;割り込み;双模倣;プログラム変換;XML, program verification;program analysis;type theory;functional programs;concurrent programs;information flow analysis

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17300003/
• 様相論理に基づいたプログラム解析手法の研究

  Grant-in-Aid for Young Scientists (B)

  Kyoto University

  五十嵐 淳

  From 01 Apr. 2003, To 31 Mar. 2006, Project Closed

  情報流解析;様相論理;非干渉性;型システム;論理関係;メタプログラミング;直観主義;不干渉性;線形時間時相論理

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15700011/
• 高級並列言語の様々な安全性を保証するプログラム進化支援つき汎用型システムの研究

  Grant-in-Aid for Young Scientists (B)

  Kyoto University;The University of Tokyo

  五十嵐 淳

  From 01 Apr. 2001, To 31 Mar. 2003, Project Closed

  型システム;並行プログラム;安全性;Java;多相性;資源使用解析;generics;プログラム進化

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13780203/
• Calculi and Logic of Environment and Context

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Masahiko SATO

  From 01 Apr. 2001, To 31 Mar. 2004, Project Closed

  対象言語;メタ言語;文法的対象;超変数;変数の衝突;文脈;環境;合流性;強正規化性;型理論;計算体系, Object Language;Meta Language;Syntactic Object;Meta Variable;Variable Collision;Context

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13480082/
• High Reliability Component-Based Software Engineering

  Grant-in-Aid for Scientific Research on Priority Areas

  Science and Engineering

  The University of Tokyo

  Tetsuo TAMAI

  From 01 Apr. 2001, To 31 Mar. 2006, Project Closed

  ソフトウェア;コンポーネント;高信頼性;再利用;モデル検査;アスペクト指向;型システム;要求仕様;Webサービス, software;component;high reliability;reuse;model checking;aspect-oriented programming;type system;requirements specification

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13224013/
• Type Systems for Secure Computing

  Grant-in-Aid for Scientific Research on Priority Areas

  Science and Engineering

  Tokyo Institute of Technology

  Naoki KOBAYASHI

  From 01 Apr. 2000, To 31 Mar. 2004, Project Closed

  型システム;セキュリティ;並行プログラム;安全性;定理証明支援器;通信の解析;計算資源;情報流解析;様相論理;Coq;Java;ライブロック, type system;security;concurrent program;safety;proof assistant;static analysis of communication;resource;information flow analysis

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-12133202/
• Memory Management Scheme Based on the Quasi-Linear Type System

  Grant-in-Aid for Scientific Research (B)

  Tokyo Institute of Technology;The University of Tokyo

  Naoki KOBAYASHI

  From 01 Apr. 1999, To 31 Mar. 2002, Project Closed

  線形型システム;擬似線形型;メモリ管理;リージョン推論;ガベージコレクション;型推論;関数型言語;資源使用解析;線形型;並列計算機;並行言語;通信チャネル, linear type system;quasi-linear types;memory management;region inference;garbage collection;type inference;functional language;resource usage analysis

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11480061/
• Implementation of Distributed Programming Languages Based on Advanced Theory for Concurrent/Distributed Computation

  Grant-in-Aid for Scientific Research (B).

  Tokyo Institute of Technology;The University of Tokyo

  Naoki KOBAYASHI

  From 01 Apr. 1998, To 31 Mar. 2001, Project Closed

  分散プログラミング言語;並行プログラミング言語;型システム;プログラム解析;デッドロック;プロセス計算;線形論理;オブジェクト指向;Java;型推論;部分評価, distributed programming;concurrency;type systems;program analysis;deadlock;process calculus;linear logic;object-oriented programming

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10558040/
• AIを含むソフトウェアのための形式検証手法

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  末永 幸平

  From 01 Apr. 2025, To 31 Mar. 2030, Granted

  形式検証;人工知能;ソフトウェア

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25H01113/

Education

Teaching subject(s)

• From 01 Apr. 2025, To 31 Mar. 2026

  Introduction to Computer Science

  9113, Spring, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Logic and Computation

  9086, Fall, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Programming Languages

  9017, Fall, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Perspective in Informatics 4

  8043, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Introduction to Computer Science

  T024, Spring, Institute for Liberal Arts and Sciences, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Introduction to Computer Science

  9113, Spring, Faculty of Engineering, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Logic and Computation

  9086, Fall, Faculty of Engineering, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Programming Languages

  9017, Fall, Faculty of Engineering, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Introduction to Computer Science

  T024, Spring, Institute for Liberal Arts and Sciences, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Programming Languages

  9017, Fall, Faculty of Engineering, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Logic and Computation

  9086, Fall, Faculty of Engineering, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Introduction to Computer Science

  9113, Spring, Faculty of Engineering, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Introduction to Computer Science

  T024, Spring, Institute for Liberal Arts and Sciences, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Logic and Computation

  9086, Fall, Faculty of Engineering, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Programming Languages

  9017, Fall, Faculty of Engineering, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Introduction to Computer Science

  9113, Spring, Faculty of Engineering, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Introduction to Computer Science

  T024, Spring, Institute for Liberal Arts and Sciences, 2
• From Apr. 2011, To Mar. 2012

  Advanced Study in IST I

  Year-long, 情報学研究科
• From Apr. 2011, To Mar. 2012

  Advanced Study in IST II

  Year-long, 情報学研究科
• From Apr. 2011, To Mar. 2012

  ソフトウェア基礎論

  Fall, 情報学研究科
• From Apr. 2011, To Mar. 2012

  知能情報学特殊研究１

  Year-long, 情報学研究科
• From Apr. 2011, To Mar. 2012

  知能情報学特殊研究２

  Year-long, 情報学研究科
• From Apr. 2011, To Mar. 2012

  計算機科学実験及演習４（計算機）

  Fall, 工学部
• From Apr. 2012, To Mar. 2013

  Foundation of Software Science

  Fall, 情報学研究科
• From Apr. 2012, To Mar. 2013

  Advanced Seminar on Intelligence Science and Technology

  Year-long, 情報学研究科
• From Apr. 2012, To Mar. 2013

  Advanced Study in Intelligence Science and Technology II

  Year-long, 情報学研究科
• From Apr. 2012, To Mar. 2013

  Advanced Study in Intelligence Science and Technology I

  Year-long, 情報学研究科
• From Apr. 2012, To Mar. 2013

  Advanced Seminar on Foundation of Software Science

  Fall, 情報学研究科
• From Apr. 2012, To Mar. 2013

  Programming Languages

  Spring, 工学部
• From Apr. 2012, To Mar. 2013

  Computer Science Laboratory and Exercise 4

  Fall, 工学部
• From Apr. 2012, To Mar. 2013

  Logic and Computation

  Fall, 工学部
• From Apr. 2013, To Mar. 2014

  Programming Languages

  Spring, 工学部
• From Apr. 2013, To Mar. 2014

  Logic and Computation

  Fall, 工学部
• From Apr. 2013, To Mar. 2014

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2013, To Mar. 2014

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2013, To Mar. 2014

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2013, To Mar. 2014

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2013, To Mar. 2014

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2013, To Mar. 2014

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2014, To Mar. 2015

  Programming Languages

  Spring, 工学部
• From Apr. 2014, To Mar. 2015

  Logic and Computation

  Fall, 工学部
• From Apr. 2014, To Mar. 2015

  Information and Business

  Spring, 工学部
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Seminar on Communications and Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Graduation Thesis 1

  Spring, 工学部
• From Apr. 2014, To Mar. 2015

  Graduation Thesis 1

  Fall, 工学部
• From Apr. 2014, To Mar. 2015

  Graduation Thesis 2

  Spring, 工学部
• From Apr. 2014, To Mar. 2015

  Graduation Thesis 2

  Fall, 工学部
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Introduction to Programming

  Spring, 工学部
• From Apr. 2015, To Mar. 2016

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Humanistic Informatics (Special Lectures)

  Spring, 文学研究科
• From Apr. 2015, To Mar. 2016

  Humanistic Informatics (Special Lectures)

  Spring, 文学部
• From Apr. 2015, To Mar. 2016

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Programming Languages

  Spring, 工学部
• From Apr. 2015, To Mar. 2016

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2015, To Mar. 2016

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2015, To Mar. 2016

  Logic and Computation

  Fall, 工学部
• From Apr. 2015, To Mar. 2016

  Seminar on Communications and Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering I

  Spring, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Introduction to Algorithms and Informatics

  Spring, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Theory of Computational Complexity

  Fall, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Introduction to Programming

  Spring, 工学部
• From Apr. 2016, To Mar. 2017

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Humanistic Informatics (Special Lectures)

  Spring, 文学研究科
• From Apr. 2016, To Mar. 2017

  Humanistic Informatics (Special Lectures)

  Spring, 文学部
• From Apr. 2016, To Mar. 2017

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Programming Languages

  Fall, 工学部
• From Apr. 2016, To Mar. 2017

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2016, To Mar. 2017

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2016, To Mar. 2017

  Logic and Computation

  Fall, 工学部
• From Apr. 2016, To Mar. 2017

  Seminar on Communications and Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering I

  Fall, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Introduction to Programming

  Spring, 工学部
• From Apr. 2017, To Mar. 2018

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Humanistic Informatics (Special Lectures)

  Spring, 文学研究科
• From Apr. 2017, To Mar. 2018

  Humanistic Informatics (Special Lectures)

  Spring, 文学部
• From Apr. 2017, To Mar. 2018

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Programming Languages

  Fall, 工学部
• From Apr. 2017, To Mar. 2018

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2017, To Mar. 2018

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2017, To Mar. 2018

  Logic and Computation

  Fall, 工学部
• From Apr. 2017, To Mar. 2018

  Seminar on Communications and Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Fall, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering I

  Spring, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Introduction to Programming

  Spring, 工学部
• From Apr. 2018, To Mar. 2019

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Media and Culture Studies (Special Lectures)

  Spring, 文学研究科
• From Apr. 2018, To Mar. 2019

  Media and Culture Studies (Special Lectures)

  Spring, 文学部
• From Apr. 2018, To Mar. 2019

  Programming Languages

  Fall, 工学部
• From Apr. 2018, To Mar. 2019

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2018, To Mar. 2019

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2018, To Mar. 2019

  Logic and Computation

  Fall, 工学部
• From Apr. 2019, To Mar. 2020

  Parallel and Distributed Systems

  Spring, 情報学研究科
• From Apr. 2019, To Mar. 2020

  Introduction to Programming

  Spring, 工学部
• From Apr. 2019, To Mar. 2020

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2019, To Mar. 2020

  Programming Languages

  Fall, 工学部
• From Apr. 2019, To Mar. 2020

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2019, To Mar. 2020

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2019, To Mar. 2020

  Logic and Computation

  Fall, 工学部
• From Apr. 2020, To Mar. 2021

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2020, To Mar. 2021

  Introduction to Programming

  Spring, 工学部
• From Apr. 2020, To Mar. 2021

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2020, To Mar. 2021

  Programming Languages

  Fall, 工学部
• From Apr. 2020, To Mar. 2021

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2020, To Mar. 2021

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2020, To Mar. 2021

  Logic and Computation

  Fall, 工学部
• From Apr. 2021, To Mar. 2022

  Introduction to Formal Languages-E2

  Spring, 全学共通科目
• From Apr. 2021, To Mar. 2022

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2021, To Mar. 2022

  System Verification

  Fall, 情報学研究科
• From Apr. 2021, To Mar. 2022

  Programming Languages

  Fall, 工学部
• From Apr. 2021, To Mar. 2022

  Introduction to Computer Science

  Spring, 全学共通科目
• From Apr. 2021, To Mar. 2022

  Introduction to Computer Science

  Spring, 工学部
• From Apr. 2021, To Mar. 2022

  Logic and Computation

  Fall, 工学部

Participation in PhD Defense

• A design and theory of strongly typed object-oriented programming languages for extensible recursive classes(拡張性の高い再帰的クラスのための型付オブジェクト指向言語の設計と理論）

  齊藤　智恵理, Sub-chief Examiner

  23 Mar. 2010
• Semantical study of intuitionistic modal logics（直観主義様相論理の意味論的研究）

  小島　健介, Sub-chief Examiner

  26 Mar. 2012
• People Detection based on Points Tracked by an Omnidirectional Camera and Interaction Distance for Service Robots System（サービスロボットシステムのための全方位カメラによるトラッキング可能特徴点とインタラクション距離情報を用いた人物検出）

  田崎　豪, Sub-chief Examiner

  24 Sep. 2013
• Computational Complexity of Tree Evaluation Problems and Branching Program Satisfiability Problems（木構造関数値評価問題と分岐プログラム充足性問題に対する計算複雑さ）

  長尾　篤樹, Sub-chief Examiner

  23 Mar. 2015
• Enhancing System Reliability using Abstraction and Efficient Logical Computation（抽象化技術と高速な論理演算を利用したシステムの高信頼化）

  沓名　拓郎, Sub-chief Examiner

  24 Sep. 2015
• An Integrated Theory of Type-Based Static and Dynamic Verification（型に基づく静的・動的検証の統合理論）

  関山　太朗, Chief Examiner

  23 Mar. 2016
• Studies on Approximation Algorithms for Bin-Packing and Train Delivery Problems （ビン詰め問題と列車配送問題に対する近似アルゴリズムの研究）

  陳　晶, Sub-chief Examiner

  23 Mar. 2016
• A Language-Based Approach to Robust Context-Aware Software（堅牢な文脈認識ソフトウェア開発のためのプログラミング言語の研究）

  井上　裕昭, Chief Examiner

  26 Mar. 2018
• Webサーバの高集積マルチテナントアーキテクチャに関する研究

  松本　亮介, Sub-chief Examiner

  23 May 2017
• ネットワーク接続された組込みシステムの拡張性に関する研究

  寺岡　秀敏, Sub-chief Examiner

  25 Mar. 2019
• Online, Submodular, and Polynomial Optimization with Discrete Structures(オンライン最適化，劣モジュラ関数最大化，および多項式関数最適化に対する離散構造に基づいたアルゴリズムの研究)

  坂上　晋作, Sub-chief Examiner

  23 Mar. 2020
• Webアプリケーションに対するサイバー攻撃の効率的な検知

  鐘本　楊, Sub-chief Examiner

  23 Mar. 2020
• Typed Software Contracts with Intersection and Nondeterminism（交差型と非決定計算を含んだ型付ソフトウェア契約）

  西田　雄気, Chief Examiner

  25 May 2020

Participation in PhD Defenses (other than KU)

• A Programming Language with Versions

  Yudai Tanabe, Tokyo Institute of Technology, Sub-chief Examiner

  Mar. 2023
• A Design and Implementation of Mixin-Based Composi- tion in Strongly Typed Object-Oriented Languages

  紙名 哲雄, 東京大学, 日本, Sub-chief Examiner

  2005
• 型理論によるJava仮想機械の形式化

  樋口 智之, 北陸先端科学技術大学院大学, 日本, Sub-chief Examiner

  2005

Student achievements: Awards

• PPL2022 発表賞(学生部門)

  Ryo Wakizaka, Mar. 2022
• 優秀発表賞

  Kosuke Umeki, 第39回日本ソフトウェア科学会大会プログラム委員会, Sep. 2022
• ベストポスター賞

  Ryo Wakizaka, QEd サマースクール2022, 03 Oct. 2022
• 2nd prize in the undergraduate category in Student Research Competition @ ACM POPL

  五十嵐 雄, ACM, Jan. 2017
• Distinguished Artifact Award

  井上 裕昭, European Conference on Object-Oriented Programming, 19 Jul. 2018
• 最優秀発表賞

  五十嵐 琢磨, 第15回 ディペンダブルシステムワークショップ (DSW 2017) , Dec. 2017
• 優秀発表賞

  矢杉 和義, 日本ソフトウェア科学会第34会大会プログラム委員会, Sep. 2017
• 優秀発表賞

  脇坂遼, 日本ソフトウェア科学会第37会大会プログラム委員会, Sep. 2020

Administration

School management (title, position)

• From 01 Apr. 2025, To 31 Mar. 2026

  研究科長部会 構成員
• From 01 Apr. 2025, To 31 Mar. 2026

  大学院教育支援機構協議会 協議員
• From 01 Apr. 2025, To 31 Mar. 2026

  教育研究評議会 評議員
• From 01 Apr. 2025, To 31 Mar. 2026

  部局長会議 構成員
• From 01 Apr. 2025, To 31 Mar. 2027

  船井哲良記念講堂・船井交流センター運営委員会 委員
• From 01 Apr. 2025, To 31 Mar. 2026

  京都大学研究資源アーカイブ運営委員会 委員
• From 01 Apr. 2025, To 31 Mar. 2026

  全学情報セキュリティ委員会常置委員会 委員
• From 01 Apr. 2025, To 31 Mar. 2026

  全学情報セキュリティ委員会 委員
• From 01 Oct. 2024, To 30 Sep. 2026

  男女共同参画推進センター魅力見える化専門部会 委員
• From 01 Oct. 2024, To 30 Sep. 2026

  技術支援企画委員会 委員
• From 01 Oct. 2024, To 30 Sep. 2026

  財務委員会 委員
• From 01 Apr. 2024, To 31 Mar. 2026

  京都大学大学院教育支援機構次世代ＡＩプログラム実施委員会 委員
• From 01 Apr. 2024, To 31 Mar. 2025

  教員活動評価委員会 委員
• From 01 Apr. 2025, To 31 Mar. 2026

  大学院情報学研究科　研究科長
• From 01 Apr. 2023, To 31 Mar. 2025

  京都大学研究資源アーカイブ運営委員会 委員
• From 01 Apr. 2024, To 31 Mar. 2026

  学生総合支援機構管理運営委員会 委員
• From 01 Apr. 2024, To 31 Mar. 2025

  全学情報セキュリティ委員会 委員
• From 01 Apr. 2023, To 31 Mar. 2025

  教育研究評議会 評議員
• From 01 Apr. 2023, To 31 Mar. 2025

  部局長会議
• From 01 Apr. 2023, To 31 Mar. 2025

  研究科長部会
• From 01 Apr. 2023, To 31 Mar. 2024

  全学情報セキュリティ委員会常置委員会 委員
• From 01 Apr. 2023, To 31 Mar. 2025

  全学情報セキュリティ委員会常置委員会 委員
• From 01 Apr. 2023, To 31 Mar. 2025

  国際高等教育院 大学院教育支援機構協議会 協議員
• From 01 Apr. 2023, To 31 Mar. 2025

  情報学研究科 研究科長
• From 01 Apr. 2023, To 31 Mar. 2025

  京都大学奨学金返還免除候補者選考委員会 委員
• From 01 Oct. 2022, To 30 Sep. 2024

  男女共同参画推進センター魅力見える化専門部会 委員
• From 01 Apr. 2023, To 30 Sep. 2024

  基金運営委員会 委員
• From 01 Apr. 2008, To 31 Mar. 2010

  情報教育専門委員会 委員
• From 01 Apr. 2014, To 31 Mar. 2016

  国際教育プログラム委員会 委員
• From 01 Apr. 2014, To 31 Mar. 2016

  国際教育プログラム委員会委員 ４号委員
• From 01 Apr. 2016, To 31 Mar. 2018

  図書館協議会 協議員
• From 19 Aug. 2016, To 31 Mar. 2018

  学際教育研究推進センター高大接続科学教育ユニットコーディネーション委員会委員
• From 01 Apr. 2020, To 31 Mar. 2022

  教育研究評議会 評議員

Faculty management (title, position)

• From 01 Apr. 2023, To 31 Mar. 2026

  桂図書館協議会協議員
• From 01 Apr. 2023, To 31 Mar. 2026

  人権委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  情報セキュリティ委員会委員長
• From 01 Apr. 2023, To 31 Mar. 2026

  評価・広報委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  基盤整備委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  財務委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  教務委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  企画委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  制規委員会委員
• From 01 Apr. 2023, To 31 Mar. 2026

  情報学研究科長
• From 01 Apr. 2022, To 31 Mar. 2026

  連携推進 ＷＧ委員
• From 01 Apr. 2022, To 31 Mar. 2023

  人権委員会委員
• From 01 Apr. 2021, To 31 Mar. 2023

  情報セキュリティ委員会委員
• From 01 Apr. 2011, To 31 Mar. 2012

  評価ＷＧ委員会委員
• From 01 Apr. 2011, To 31 Mar. 2013

  計算機小委員会委員
• From 01 Apr. 2012, To 31 Mar. 2013

  情報セキュリティ作業委員会委員
• From 01 Apr. 2013, To 31 Mar. 2014

  財務委員会委員
• From 01 Apr. 2014, To 31 Mar. 2015

  教務委員会委員長
• From 01 Apr. 2015, To 31 Mar. 2016

  制規委員会副委員長
• From 01 Apr. 2015, To 31 Mar. 2016

  情報セキュリティ委員会委員
• From 01 Apr. 2016, To 31 Mar. 2017

  制規委員会委員長
• From 01 Apr. 2017, To 31 Mar. 2018

  評価・広報委員会委員長
• From 01 Apr. 2017, To 31 Mar. 2018

  制規委員会副委員長
• From 01 Apr. 2017, To 31 Mar. 2018

  専攻長会議
• From 01 Apr. 2018, To 31 Mar. 2019

  情報セキュリティ委員会委員
• From 01 Apr. 2018, To 31 Mar. 2019

  専攻長
• From 01 Apr. 2018, To 31 Mar. 2019

  制規委員会委員長
• From 01 Apr. 2016, To 31 Mar. 2020

  教育用計算機専門委員会委員
• From 01 Apr. 2019, To 31 Mar. 2020

  制規委員会委員長
• From 01 Apr. 2019, To 31 Mar. 2020

  工学部教育制度委員会　委員
• From 01 Apr. 2020, To 31 Mar. 2023

  副研究科長
• From 01 Apr. 2020, To 31 Mar. 2023

  企画委員会委員長
• From 01 Apr. 2020, To 31 Mar. 2022

  財務委員会委員
• From 01 Apr. 2020, To 31 Mar. 2022

  人を対象とする研究倫理小委員会委員