The combination of deep theoretical insights and practical tool development results in a milestone for quantum circuit verification.

The framework leverages tree automata to compactly represent sets of quantum states; transformers implement the semantics of quantum gates over this representation.

The accompanying paper asks whether we can internalize in logic the property known as “Church’s Thesis.”

The compatibility of ​the Church thesis with dependent type theory was an open question. In this paper, we answer this question positively.

Formal computer science may never model practical computer engineering well enough to be predictive in the way the physical sciences are.