Paper: Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions (at LICS 2026)

Authors: Gilles Barthe Minbo Gao Jam Kabeer Ali Khan Matthijs Muis Ivan Renison Keiya Sakabe Michael Walter Yingte Xu Tianshi Yu Li Zhou

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.15

Abstract

We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

BibTeX

  @InProceedings{BartheGaoKhanMuisRe-CompleteRelationalL,
    author = 	 {Gilles Barthe and Minbo Gao and Jam Kabeer Ali Khan and Matthijs Muis and Ivan Renison and Keiya Sakabe and Michael Walter and Yingte Xu and Tianshi Yu and Li Zhou},
    title = 	 {Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {15:1--15:28},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.15}
  }