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

题目:量子程序及其验证

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

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

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

地点:太阳城娱乐城 A201

主持:李绿周副教授

摘要:量子硬件设计和制造技术的快速发展使得有可能在5 - 10年内实现特定用途的量子计算机。那时,量子程序将成为真正发挥量子计算机作用的关键。由于量子计算机和传统计算机在信息处理方面存在本质区别(例如量子信息的不可克隆性和纠缠的非局部效应),量子程序的设计将是一个非常困难且容易出错的过程,即使完全需要A与经典编程不同的思维方式。因此,一套有效的分析和验证技术对于确保量子程序的正确性尤为重要。本报告介绍了编程语言中简单量子的语法和语义(包括结构化操作语义和参考语义)。在此基础上,介绍了该语言中量子程序正确性的定义及其验证技术。

个人简介:冯远,男,澳大利亚悉尼科技大学机械与信息技术学院教授。他分别于1999年和2004年毕业于清华大学,获得理学学士学位和工程博士学位。 2004年8月,他进入清华大学计算机科学系智能技术与系统国家重点实验室。 2007年12月,他晋升为副研究员。自2009年1月起,他一直担任悉尼科技大学量子计算和智能系统研究中心的高级讲师。 2015年1月,他被提升为教授,并被授予2010年澳大利亚研究理事会ARC未来奖学金。主要从事理论计算机科学,量子信息处理,量子程序理论等方面的研究。博士论文《量子信息的分辨、克隆、删除与纠缠转化》获得2006年全国杰出博士论文奖。 ACM Trans。编程语言和系统,ACM Trans。关于计算逻辑,IEEE Trans。关于软件工程,IEEE Trans。信息论,IEEE Trans。计算机,信息与计算,计算机与系统科学期刊,物理评论快报等计算机科学与量子计算领域的国际权威期刊,以及POPL,ICSE,CONCUR等主要国际会议发表的70多篇学术论文,MFCS和CSF。