计算之智与哲学之慧分享 http://blog.sciencenet.cn/u/huangfuqiang

博文

耶鲁大学邵中教授20100108

已有 9642 次阅读 2010-1-8 11:54 |个人分类:计算机软件理论与工程|系统分类:人物纪事| 耶鲁大学邵中教授

信息来源于: http://www.ustcif.org/default.php/content/266/
8311 邵中

邵中,毕业于江苏省常熟中学,1983年考入中国科学技术大学少年班,1987年获得郭沫若奖学金,1988年获得计算机科学系学士学位。同年被美国普林斯顿大学录取,1991年获得硕士学位,1994年获得博士学位。

1994年博士毕业后,邵中被聘为美国耶鲁大学计算机科学系助理教授,2000年被提为副教授,2003年7月起,他晋升为耶鲁大学计算机系正教授,此时他尚未度过自己的35周岁生日。

邵中教授是计算机程序语言设计和实现领域国际权威。他曾任ACM SIGPLAN 执行委员会委员,并担任程序设计语言领域多种一流国际会议和期刊的评审委员会委员和编委。2005年起他兼任中国科大客座教授, 清华大学姚期智小组讲席教授, 及中华全国青联第十届委员会常务委员。


图片来源:软件学院苏州项目部
以下信息来源于中科大

邵中教授是耶鲁大学教授、中国科大大师讲席教授、兼职博士生导师。他的科研工作和成果简介如下:

是学术界和工业界科研项目中广泛使用的SML/NJ函数式编程语言的编译器的主要设计和实现者之一,其中有影响的研究成果包括基于后续传递风格的编译方法等多项成果。

研究和开发了保类型的编译器基础构造FLINT,其中最显著的贡献是用高阶lambda演算对多种差异明显的源语言的类型系统进行编码,使得类型检查可以在编译的任何阶段进行。

近年来,研究重点集中在开发新的程序验证理论和技术,目标是为开发经过验证的大规模系统软件构建一种实用的基础平台。提出了领域专用语言加领域专用逻辑来验证领域专门代码并连接它们成为完整的经过验证的软件系统的思想和方法。已经开创性地设计了验证操作系统若干部分所需的多种专用逻辑和连接各种证明的开放框架,完成了汇编代码级的垃圾收集和存储分配等库函数、自修改代码的引导程序、非抢占式并发线程等实例程序的验证,最近验证了一个带硬中断和抢占式并发的简单操作系统。


个人主页

https://blog.sciencenet.cn/blog-89075-285276.html

上一篇:分离逻辑(separation logic)创始人20100107
下一篇:算法的威力:程序员用台式机打破超级计算机保持的世界记录20100109
收藏 IP: .*| 热度|

1 盖鑫磊

该博文允许实名用户评论 评论 (3 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-5-20 20:46

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部