邵中

研究方向：高可信软件、程序设计语言及编译、操作系统　邵中,男，1968年8月生，耶鲁大学教授，中国科大“大师讲席”教授。1983年进入中国科学技术大学少年班，1988年毕业于计算机系，获计算机科学学士学位；1994年毕业于普林斯顿大学，获计算机科学博士学位。1994年起至今在耶鲁大学计算机系任教，2003年起任耶鲁大学教授。现任中科大－耶鲁高可信软件联合研究中心主任。　是学术界和工业界科研项目中广泛使用的SML/NJ函数式编程语言的编译器的主要设计和实现者之一，其中有影响的研究成果包括基于后续传递风格的编译方法等多项成果。　研究和开发了保类型的编译器基础构造FLINT，其中最显著的贡献是用高阶lambda演算对多种差异明显的源语言的类型系统进行编码，使得类型检查可以在编译的任何阶段进行。　近年来，研究重点集中在开发新的程序验证理论和技术，目标是为开发经过验证的大规模系统软件构建一种实用的基础平台。提出了领域专用语言加领域专用逻辑来验证领域专门代码并连接它们成为完整的经过验证的软件系统的思想和方法。已经开创性地设计了验证操作系统若干部分所需的多种专用逻辑和连接各种证明的开放框架，完成了汇编代码级的垃圾收集和存储分配等库函数、自修改代码的引导程序、非抢占式并发线程等实例程序的验证，最近验证了一个带硬中断和抢占式并发的简单操作系统。　主要学术任职：1．2009年起，担任ACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL)指导委员会主席2．担任第36届ACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL’09)大会主席3．担任第5届AsianSymposiumonProgrammingLanguagesandSystems(APLAS’07)大会程序主席4．各种国际学术会议和学术讨论会的程序委员会委员，包括：SSV’09，POPL’08，SSV’08，TASE’07，TFP’07，CC’07，APLAS’06，ATVA’06，TFP’06，POPL’05，ICFP’03，APLAS’03，PLDI’99，TIC’98，POPL’965．各种学术杂志的编委，包括：JournalofFunctionalProgramming(2001–)，JournalofComputingScienceandEngineering(2007–)，JournalofComputerScienceandTechnology(2006–)6.2001–2005，ACMSIGPLAN执行委员会学术委员（MembersatLarge）　　获奖情况1．1988年中国科学技术大学郭沫若奖学金2．1995－1998年美国国家科学基金青年学者奖　主要论著/