LAB LOG评价网站 LabLog 的页面
理论计算机科学・编程语言理论・类型理论（Jacques Garrigue）
机器翻译 · 查看原文
给程序加上“类型”，在不损失表达力的前提下消除bug的语言理论。
About关于研究室
用类型与证明，打造没有bug的程序。
Jacques Garrigue老师研究编程语言理论。
其目标是在不损害编程语言表达力的前提下，
主要研究对象是类型系统和程序证明。
同时也尝试将Coq这一定理证明辅助系统应用于数学和系
术语说明
- 类型系统
- 为数据和函数加上“类型”
（整数、 字符串等）， 在运行前发现错误用法的 机制 - 类型推断
- 由计算机自动补全程
序中 未写出的类型信息的机制 - 定理证明辅助系统
- 用于在计算机上一步一步严格验证数学证明或程
序正确性的软件
Research研究课题
以在
※示意图类型系统与类型推断
作为函数式编程语言OCaml的开发者之一，
※示意图用证明来验证语言的实现
由于难以保
※示意图定理证明辅助系统的应用
与产业技术综合研究所的研究人员和名古屋大学的学生一起，
※示意图量子程序的证明
从几年前开始对量子计算也产生了兴趣。
Members教师
- 教授Jacques Garrigue
Voices学长学姐的评价
评价基于在读
对于接受采访的学生，
学长学姐的评价
--
--
--
--
--
--
学长学姐的评价会回答这些问题
- 这个研究室的推荐点是什么?
- 进入后才知道的事情是什么?
- 氛围和老师的性格如何?
- 推荐给什么样的学生?
- 毕业后的去向?
Related与理论计算机科学・编程语言理论・类型理论（Jacques Garrigue）相似的研究室
表现论・算子代数
Henrik Bachmann研究室理学部 数理学科我对与多重zeta值和模形式理论相关的各种课题感兴趣。
木下研究室理学部 数理学科偏微分
森吉 仁志研究室理学部 数理学科研究流形的拓扑，本页信息由LabLog运营团队根据研究室的公开信息和采访整理。
关于图片
顶部和研究课题的图片为示意图，
- 顶部图片：《VS Code Screenshot》 Cycling2／CC0（裁剪）
- 类型系统与类型推断：《Code on computer monitor (Unsplash)》 Markus Spiske markusspiske／CC0（裁剪）
- 用证明来验证语言的实现：《Closeup of keys》 John Snyder／CC BY-SA 4.0（裁剪）
- 定理证明辅助
系统的应用：《YunTech Computer Classroom 20220612》 S099001／CC BY 4.0（裁剪） - 量子程序的
证明：《Quantum-computer-Chalmers 2017》 Anita Fors (Chalmers)／CC BY-SA 4.0（裁剪） - 相关研究室
（表现论・算子代数 （荒野 悠輝）） ：《Mathematics lecture notes, Mathematical analysis, Linear algebra, Rostov-on-Don, Russia》 Vyacheslav Argenberg／CC BY 4.0（裁剪） - 相关研究室
（Henrik Bachmann研究室） ：《ZetaFunction》 Gaussianer／公有领域 （裁剪） - 相关研究室
（木下研究室） ：《Unusual wave at the Gap》 Avenue／CC BY-SA 3.0（裁剪） - 相关研究室
（森吉 仁志研究室） ：《Surface of revolution illustration》 Oleg Alexandrov／公有领域 （裁剪）
关于 LabLog
LabLog 是学生专属的研究室评价应用。
本页的研究室基本信息和评分汇总与 LabLog 介绍允许搜索引擎和 AI 引用。