Pith. sign in

REVIEW

Formal Semantics of a Classical-Quantum Language

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2107.00804 v1 pith:TEWNCKM7 submitted 2021-07-02 cs.LO

Yuxin Deng , Yuan Feng This is my paper
classification cs.LO
keywords semanticsproofabstractconcreteformallanguagesoundsystems
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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.

Discussion (0). Sign in to comment.

Pith tools