Verification Series
2026-03-19 11:00 - 12:00 | Ashton 208
Alexei Lisitsa: Quantum verification via tangles, quandles, and automated reasoning

In this talk, I will present our recent work on automating the verification of

quantum programs and circuits, building on a method proposed by Reutter and

Vicary (2019). In this framework, quantum circuits and programs are modelled as

tangles—informally, finite collections of strings or laces embedded and

entangled in three-dimensional space. Verification of program equivalence is

then reduced to the problem of tangle equivalence (isotopy), yielding a

conceptually simple and visually appealing approach.

Drawing on our earlier work on applying automated reasoning to computational

topology, particularly knot theory, we translate the resulting topological

problems into an algebraic setting. This is achieved using variants of

algebraic structures known as quandles. Automated reasoning tools (theorem

provers and model finders) are then employed to establish (non-)equivalence of

tangles, and hence of the corresponding quantum circuits.

I will conclude by highlighting several open questions and challenges, both in

the theoretical foundations of the approach and in its practical application to

quantum program verification.

Joint work with Andrew Fish.

https://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1334
