高木 翼（准教授）
联系方式
- 工作单位：北陆先端科学技术大学院大学（JAIST），信息科学学院，计算科学领域
- 电子邮件地址：
- 研究室：I-54b（信息科学研究大楼5层）
- 办公时间：每周一下午三时至四时（在此时间内来访者勿需提前预约）
- 有意参观或加入研究室者，请先通过电子邮件咨询（也可在线面谈）。
研究领域
我们研究室的研究领域是理论计算机科学。 在信息技术发达的当今社会，每个人都在使用智能手机和个人电脑等广义上的“计算机”来丰富自己的生活。 在我们研究室，我们并不局限于将“计算器”作为单纯的工具，而是研究从理论上将其构造重新构建和设计新的方案。
具体来说，我们应用数学的一个分支--数理逻辑，科学地探索编程功能以及软件和通信协议的规范。 更进一步，在此研究成果基础上，我们的目标是通过开发一种名为形式验证的技术来实现高可靠性软件，该技术可从数学上保证算法和程序的正确性。
关键词：形式化规范/验证、多类等式逻辑、模态逻辑、动态逻辑（霍尔逻辑）、时间逻辑（模型检查）、量子逻辑、泛代数、变迁系统、并发计算、量子计算、量子程序/协议
研究立场
- 基本从定义、定理和证明展开讨论。
- 不过，研究动机不在数学，而在计算机科学。
- 也会编程来证明理论的有效性。
学生指导方针
- 最大程度地考虑每个学生的背景（本科阶段学习了什么、优势和劣势等）和动机（想要研究什么、想要学习什么等）。
- 没有理论基础的学生将从数学基础开始指导。
- 重视独立、自主和自由的精神，目标是成为一个开放的研究室。
研究者研究前人从未提出过的新式编程、规格描述、系统开发或定式化。 在我们的研究室，研究者应在不断积累数学基础知识之上，建立和完善面向应用和实际（而不仅仅是为理论而理论）的新理论。 我们的目标是构建能够影响百年后社会的精密理论。
培养高度专业化的技术人才超过一定水平的技术人员需要具备高度的专业知识。 具体来说，他们不仅要会编程和编写规范，还需通过数学方式严格理解其工作原理和功能。 在我们的研究室，我们使用函数式编程语言设计命令式编程语言的解释器和编译器，编写基于类型论和通用代数的形式化规范，并分析通信协议和分布式系统（模型检查）。
关于学生生活
- 除了每周的学习/研究进度汇报会之外，学生没有必须参加的活动。
- 研究室的来去时间没有强制要求。
- 如有必要，可以组织基础知识学习会和研究室合宿（自由参加）。
- 不会在忙于找工作或回家的时期强制学生研究。
- 对于希望更认真学习的学生，有长期学习制度（以两年的学费在学三年）。
- 如果预算允许，学生可以被聘为研究室助理（LA）或研究助理（RA）获得酬金。
- 有意愿的博士生可以被聘为大学助理（UA）获得酬金。
- 被选为JSPS研究员或JAIST下一代研究员的博士生可以在获得生活费和研究费的支持下全身心投入研究（请参阅奖学金信息）。
成员
- 高木 翼（准教授）
- 宋阳（研究員）
- 小林 脩亮（M1）
- 中村 太陽（M1）
- 名越 龍一（M1）
- 山口 快（M1）