We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states . We develop a program logic where pre- and post-conditions are BI formulas describing quantumstates . We exercise logic for proving the security of quantum one-time pad and secret sharing . We show how the program logic can be used to discover a flaw in Google Cirq’s tutorial on the VariationalQuantum Algorithm (VQA)

Author(s) : Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu

Links : PDF - Abstract

Code :

Keywords : logic - quantum - program - bunched - bi -

Leave a Reply

Your email address will not be published. Required fields are marked *