报告题目：Reasoning about Parallel Quantum Programs: Some New Results.

报告人：    应明生 悉尼科技大学杰出教授

主持人：    邓玉欣 教授

报告时间：2019年9月18日 周三10:00-11:00   

报告地点：理科大楼B1002

报告摘要：

We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) finding a series of useful proof rules for reasoning about correctness of parallel quantum programs; (2) proving a (relative) completeness of our proof rules for partial correctness of disjoint parallel quantum programs; and (3) proving a strong soundness theorem of the proof rules showing that partial correctness is well maintained at each step of transitions in the operational semantics of a general parallel quantum program (with shared variables). This is achieved by partially overcoming the following conceptual challenges that are never present in classical parallel programming: (i) the intertwining of nondeterminism caused by quantum measurements and introduced by parallelism; (ii) entanglement between component quantum programs; and (iii) combining quantum predicates in the overlap of state Hilbert spaces of component quantum programs with shared variables. Applications of the techniques developed in this paper are illustrated by a formal verification of Bravyi-Gosset-König’s parallel quantum algorithm solving a linear algebra problem, which gives for the first time an unconditional proof of a computational quantum advantage.

报告人简介：

应明生教授是悉尼科技大学杰出教授（UTS Distinguished Professor）和中科院软件所学术副所长。他曾是清华大学计算机科学与技术系教授、博士生导师、教育部“长江学者奖励计划”特聘教授、智能技术与系统国家重点实验室学术委员会主任。1994年被人事部批准为中青年有突出贡献专家，获第4届中国青年科技奖，1997年获国家杰出青年科学基金，入选教育部跨世纪优秀人才培养计划。主要从事形式化方法、量子计算与量子信息、人工智能基础理论等方面的科研工作，著有《Topology in Process Calculus》和《Foundations of Quantum Programming》两本专著，在著名国际期刊和会议发表一百多篇论文。担任Artificial Intelligence等刊物编委、International Fuzzy Systems Association副主席、复旦大学兼职教授、华东师范大学上海市高可信计算重点实验室学术委员会成员。