2021/07/02 by Yuxin Deng, Yuan Feng, Deng, Yuxin +1
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2107.00804
openalex publication_date 2021/07/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.