邵中(教授)的个人简介
邵中,男,中国科大“大师讲席”教授。1983年进入中国科学技术大学少年班,1988年毕业于计算机系,获计算机科学学士学位;1994年毕业于普林斯顿大学,获计算机科学博士学位。1994年起至今在耶鲁大学计算机系任教,2003年起任耶鲁大学教授。现任中科大-耶鲁高可信软件联合研究中心主任。是学术界和工业界科研项目中广泛使用的SML/NJ函数式编程语言的编译器的主要设计和实现者之一,其中有影响的研究成果包括基于后续传递风格的编译方法等多项成果。研究和开发了保类型的编译器基础构造FLINT,其中最显著的贡献是用高阶lambda演算对多种差异明显的源语言的类型系统进行编码,使得类型检查可以在编译的任何阶段进行
个人简介
近年来,研究重点集中在开发新的程序验证理论和技术,目标是为开发经过验证的大规模系统软件构建一种实用的基础平台。提出了领域专用语言加领域专用逻辑来验证领域专门代码并连接它们成为完整的经过验证的软件系统的思想和方法。已经开创性地设计了验证操作系统若干部分所需的多种专用逻辑和连接各种证明的开放框架,完成了汇编代码级的垃圾收集和存储分配等库函数、自修改代码的引导程序、非抢占式并发线程等实例程序的验证,最近验证了一个带硬中断和抢占式并发的简单操作系统。
主要学术任职
1.2009年起,担任A CMSIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL)指导委员会主席
2.担任第36届A CMSIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPLu201909)大会主席
3.担任第5届Asian Symposium on Programming Language sand Systems(APLASu201907)大会程序主席
4.各种国际学术会议和学术讨论会的程序委员会委员,包括:SSVu201909,POPLu201908,SSVu201908,TASEu201907,TFPu201907,CCu201907,APLASu201906,ATVAu201906,TFPu201906,POPLu201905,ICFPu201903,APLASu201903,PLDIu201999,TICu201998,POPLu2019965.各种学术杂志的编委,包括:Journal of unctional Programming(2001u2013),Journal of Computing Science and Engineering(2007u2013),Journal of Computer Science and Technology(2006u2013)6.2001u20132005,ACMSIGPLAN执行委员会学术委员(Membersat Large)
主要研究方向
高可信软件、程序设计语言及编译、操作系统
获奖情况
1.1988年中国科学技术大学郭沫若奖学金
2.1995-1998年美国国家科学基金青年学者奖