学术报告:量子程序及其验证

题目:量子程序及其验证

主讲人:冯元( 悉尼科技大学,教授)

日期:2018年11月30日(星期五)

时间:上午9:30 - 10:30

地点:数据科学与计算机学院 A201

主持:李绿周副教授

 

摘要:量子硬件设计与制造技术的飞速发展使得特定用途的量子计算机有望在5-10年内实现,届时量子程序将成为真正发挥量子计算机作用的关键。由于量子计算机和传统计算机在信息处理方面有着本质的区别(比如量子信息的不可克隆性和纠缠的非局域作用等特征),量子程序的设计将是一个非常困难而容易犯错的过程,甚至需要和经典程序设计完全不同的思维方式。因此,一套行之有效的分析和验证技术对于保证量子程序的正确性就显得尤为重要。本报告将介绍一种简单量子while程序语言的语法和语义(包括结构化操作语义和指称语义)。在此基础上,介绍该语言下量子程序的正确性定义及其验证技术。

 

个人介绍:冯元,男,澳大利亚悉尼科技大学机械与信息技术学院教授。分别于1999年和2004年毕业于清华大学应用数学系和计算机系,获理学学士和工学博士学位。2004年8月进入清华大学计算机系智能技术与系统国家重点实验室工作。2007年12月晋升为副研究员。2009年1月起任悉尼科技大学量子计算与智能系统研究中心高级讲师,2015年1月晋升为教授,获2010年澳大利亚研究理事会ARC Future Fellowship。主要从事理论计算机科学、量子信息处理、量子程序理论等方面的研究。博士学位论文《量子信息的分辨、克隆、删除与纠缠转化》获2006年度全国百篇优秀博士论文奖。已在 ACM Trans. on Programming Languages and Systems, ACM Trans. on Computational Logic, IEEE Trans. on Software Engineering, IEEE Trans. on Information Theory,IEEE Trans. on Computers, Information and Computation, Journal of Computer and System Sciences, Physical Review Letters等信息、计算机科学和量子计算领域国际权威期刊和POPL、ICSE、CONCUR、MFCS、CSF等知名国际会议发表学术论文70余篇。