We add local variables to quantum relational Hoare logic (Unruh, POPL 2019). We derive reasoning rules for supporting local variables (including an improved "adversary rule"). We extended the qrhl-tool for computer-aided verification of qRHL to support local variables and our new reasoning rules.

翻译：我们把本地变量添加到量子关系Hoare逻辑(Unruh, POPL 2019 ) 。 我们为支持本地变量制定推理规则(包括改进的“逆向规则 ” ) 。 我们扩展了qRHL计算机辅助验证工具,以支持本地变量和我们新的推理规则。