冯元，清华大学教授。曾任悉尼科技大学工程与信息技术学院高级讲师、副教授、教授，主要从事量子计算与量子信息处理、量子模型检测、量子程序验证、量子通信并发系统等方面的研究。在剑桥大学出版社出版量子模型检测领域第一本学术专著，在国际权威期刊和会议发表学术论文100余篇。现任ACM Transactions on Software Engineering and Methodology编委。曾获全国百篇优秀博士论文奖、澳大利亚研究理事会Future Fellowship，2023年入选国家海外高层次人才计划。

孙晓明，中国科学院计算技术研究所研究员，量子计算与算法理论实验室主任，国家杰出青年科学基金获得者。主要研究领域为算法与计算复杂性、量子计算等，曾获王选杰出青年学者奖等。目前担任《中国科学：信息科学》《软件学报》，Information and Computation，JCST等杂志编委，工业和信息化部信息通信科学技术委员会委员，曾任CCF理论计算机科学专委主任。

报告主题：量子线路综合优化中的一类数学问题

摘要：量子线路是描述量子算法的通用数学模型和具体实现方案，当前量子计算的研究已经进入含噪声中等尺度量子系统（NISQ）阶段，对量子线路的优化是NISQ阶段量子计算研究的一个热点。在这一报告中我们将汇报近期在量子电路优化方面的一些工作进展，并介绍由此抽象出来的一般化的数学问题及其相关研究进展。

邓玉欣，华东师范大学教授，上海市高可信计算重点实验室主任。主要研究方向包括并发计算模型、程序理论、量子计算，代表性工作包括一个已经被国外学者写进教科书的“邓引理”(Deng Lemma)和关于概率并发理论的一部英文专著。发表学术论文100余篇，出版教材1本。曾为CONCUR 2018作特邀报告。在40余次国际会议中任程序委员会委员。担任期刊Scientific Annals of Computer Science编委。

报告主题：量子程序的形式化验证

摘要：本报告介绍量子程序验证的三种形式化方法：互模拟检验、定理证明和霍尔逻辑。首先，我们利用基互模拟描述量子CCS进程的行为等价关系，实现了判定算法，并开发了一款工具，可以验证量子通信协议的正确性。其次，我们提出一种关于量子电路正确性的符号推理方法。它基于一组涉及向量和矩阵的基本定律，扩展性好，适合在定理证明器Coq中实现自动化。最后，我们提出了一种新的量子霍尔逻辑，通过引入分布公式来描述概率性质，方便概率行为的局部推理，特别是验证了包括HHL和Shor算法在内的典型量子算法的正确性。

周立，CCF量子计算专业委员会执行委员，中国科学院软件研究所副研究员。2019年获得清华大学计算机系博士学位，之后赴德国马克斯普朗克安全与隐私研究所做博士后。主要研究方向为量子程序设计方法学，包括对量子程序的验证、计算机辅助证明等。近年来多个原创性工作发表于POPL、PLDI、LICS等顶级会议。与合作者共同开发首个实用的后量子密码协议验证工具EasyPQC与首个经过验证的量子程序验证平台CoqQ。

报告主题：量子分离逻辑：含堆操作的量子程序验证

摘要：量子程序内存管理对提高量子资源使用率至关重要。我们重新审视高级语言中内存分配操作的语义，即，可以获得一个新的可能处于任意状态而非0态的量子比特。这允许量子dirty辅助比特——一种从其他进程中临时借用量子比特的技术——在高级语言中的实现，由此显著降低系统对量子比特资源的需求。我们提出BI风格的量子断言逻辑，并建立具有相对完备性的量子分离逻辑。该逻辑可严格证明对dirty辅助比特的正确使用，以及推理带有量子内存分配与释放的量子程序。

卢丽强，本科与博士毕业于北京大学，毕业后加入浙江大学计算机学院。研究方向为量子计算机体系结构、人工智能芯片、软硬件协同优化等。近五年发表20余篇体系结构领域CCF-A类论文，包括ISCA、HPCA、MICRO、ASPLOS，并在MICRO 2021、ASPLOS 2024做tutorial报告（中国大陆首次在体系结构四大会上组织量子计算相关tutorial），主持国家重点研发计划-青年科学家项目。曾获得全球可持续发展青年、华为天才少年第一档、CCF体系结构优博、北京大学优博等荣誉。于2022年7月发布了基于浙江大学自研天目量子芯片的全栈式量子计算云平台——太元一号量子云平台，集成了可视化编程框架、量子编译工具链、量子操作系统等核心组件。

报告主题：全栈式量子体系结构——JanusQ太元量子计算研究与实践

摘要：随着量子芯片工艺和量子算法的快速发展与深入研究，量子计算机体系结构正在得到越来越多人的关注。报告介绍浙江大学研制的太元量子云平台及在全栈式量子体系结构领域的研究进展。针对硬件测控系统，围绕量子计算读取校准与量子波形IO带宽优化，提出张量积迭代分解理论与波形动态缓存库技术，能够大幅度提升读取精度，同时将校准时延、波形传输时延大幅降低；围绕软件编译优化，提出基于电路拓扑特征与上下文结构的分析框架，框架基于向量化的电路表征方法，能够用于各类量子电路分析优化下游任务，可大幅提升电路分析精度、缩短电路综合时间；同时，面向可满性问题(SAT)与化学分子模拟，提出了领域相关的量子软硬件协同优化技术，并实现了端到端的量子加速。