We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an abstract one and a concrete one. The two proof systems are satisfaction-based, as inspired by the program logics of Barthe et al for probabilistic programs. The abstract proof system turns out to be sound and relatively complete, while the concrete one is sound only.


翻译:我们调查了一种具有古典和量子构造的简单必要语言的正式语义。 更具体地说,我们提供了一种实用的语义、一种省略语义和两种Hoare式的验证系统:一种抽象的,一种具体的。 两种验证系统都是基于满意度的,这是由Barthe et al 的程序逻辑所启发的概率程序。 抽象的验证系统是健全和相对完整的,而具体系统则只是健全的。

0
下载
关闭预览

相关内容

专知会员服务
123+阅读 · 2020年9月8日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
意识是一种数学模式
CreateAMind
3+阅读 · 2019年6月24日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
(TensorFlow)实时语义分割比较研究
机器学习研究会
9+阅读 · 2018年3月12日
Python机器学习教程资料/代码
机器学习研究会
8+阅读 · 2018年2月22日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年9月6日
Arxiv
0+阅读 · 2021年9月6日
Arxiv
4+阅读 · 2019年9月5日
VIP会员
相关主题
相关资讯
意识是一种数学模式
CreateAMind
3+阅读 · 2019年6月24日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
(TensorFlow)实时语义分割比较研究
机器学习研究会
9+阅读 · 2018年3月12日
Python机器学习教程资料/代码
机器学习研究会
8+阅读 · 2018年2月22日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员