Reasoning About Imperative Quantum Programs

被引：39
作者：
Chadha, R. [1 ]
Mateus, P. [1 ]
Sernadas, A. [1 ]
机构：
[1] Inst Super Tecn, CLC, Dept Math, Lisbon, Portugal
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2006年 / 158卷
关键词：
Quantum imperative programs; exogenous semantics; Hoare logic;
D O I：
10.1016/j.entcs.2006.04.003
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A logic for reasoning about states of basic quantum imperative programs is presented. The models of the logic are ensembles obtained by attaching probabilities to pairs of quantum states and classical states. The state logic is used to provide a sound Hoare-style calculus for quantum imperative programs. The calculus is illustrated by proving the correctness of the Deutsch algorithm.
引用
收藏
页码：19 / 39
页数：21
相关论文
共 33 条
[1]   DECIDABILITY AND EXPRESSIVENESS FOR 1ST-ORDER LOGICS OF PROBABILITY [J].
ABADI, M ;
HALPERN, JY .
INFORMATION AND COMPUTATION, 1994, 112 (01) :1-36
[2]   A categorical semantics of quantum protocols [J].
Abramsky, S ;
Coecke, B .
19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, :415-425
[3]  
Adao P., 2005, 3 INT WORKSH QUANT P
[4]  
Altenkirch T, 2005, IEEE S LOG, P249
[5]  
Baltag A., 2006, MATH STRUCTURES COMP
[6]  
Chadha R., 2005, PREPRINT, P1049
[7]  
Chadha R., 2006, REASONING STAT UNPUB, P1049
[8]  
D'Hondt E., 2004, P 2 INT WORKSH QUANT, V33, P75
[9]  
Den Hartog J. I., 2002, International Journal of Foundations of Computer Science, V13, P315, DOI 10.1142/S012905410200114X
[10]   QUANTUM-THEORY, THE CHURCH-TURING PRINCIPLE AND THE UNIVERSAL QUANTUM COMPUTER [J].
DEUTSCH, D .
PROCEEDINGS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 1985, 400 (1818) :97-117
1234