We study the two dual quantum information effects to manipulate the amount of information in quantum computation: hiding and allocation. The resulting type-and-effect system is fully expressive for irreversible quantum computing, including measurement. We provide universal categorical constructions that semantically interpret this arrow metalanguage with choice, starting with any rig groupoid interpreting the reversible base language. Several properties of quantum measurement follow in general, and we translate (noniterative) quantum flow charts into our language. The semantic constructions turn the category of unitaries between Hilbert spaces into the category of completely positive trace-preserving maps, and they turn the category of bijections between finite sets into the category of functions with chosen garbage. Thus they capture the fundamental theorems of classical and quantum reversible computing of Toffoli and Stinespring.
Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Quantum Information EffectsRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson POPL Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI Media Attached | ||
11:10 25mResearch paper | A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote POPL Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University DOI Media Attached | ||
11:35 25mResearch paper | Semantics for Variational Quantum ProgrammingRemote POPL Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria DOI Media Attached |