sync with PACMPL articles from 2024 and 2025

Author: k4rtik

content/publication/Abdulla2025/cite.bib

@@ -0,0 +1,20 @@
+@article{Abdulla2025,
+ title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata},
+ author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun},
+ year = {2025},
+ month = {January},
+ journal = {Proceedings of the ACM on Programming Languages},
+ publisher = {{Association for Computing Machinery}},
+ address = {New York, NY, USA},
+ volume = {9},
+ number = {POPL},
+ eid = {32},
+ pages = {32},
+ numpages = {31},
+ doi = {10.1145/3704868},
+ abstract = {We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices, which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification, i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches. We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.},
+ keywords = {quantum circuits, tree automata, verification},
+ webnote = {POPL '25},
+ bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
+}
+

content/publication/Abdulla2025/index.md

@@ -0,0 +1,62 @@
+---
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: Verifying Quantum Circuits with Level-Synchronized Tree Automata
+subtitle: ''
+summary: ''
+authors:
+- Parosh Aziz Abdulla
+- Yo-Ga Chen
+- Yu-Fang Chen
+- Luk'avs Hol'ik
+- Ondvrej Leng'al
+- Jyun-Ao Lin
+- Fang-Yi Lo
+- Wei-Lun Tsai
+tags:
+- quantum circuits
+- tree automata
+- verification
+categories: []
+date: '2025-01-01'
+lastmod: 2025-08-20T07:44:16-05:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '2'
+abstract: We present a new method for the verification of quantum circuits based on
+  a novel symbolic representation of sets of quantum states using level-synchronized
+  tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition
+  with a set of choices, which are then used to synchronize subtrees of an accepted
+  tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive
+  power while maintaining important properties, such as closure under union and intersection,
+  and decidable language emptiness and inclusion. We have developed an efficient and
+  fully automated symbolic verification algorithm for quantum circuits based on LSTAs.
+  The complexity of supported gate operations is at most quadratic, dramatically improving
+  the exponential worst-case complexity of an earlier tree automata-based approach.
+  Furthermore, we show that LSTAs are a promising model for parameterized verification,
+  i.e., verifying the correctness of families of circuits with the same structure
+  for any number of qubits involved, which principally lies beyond the capabilities
+  of previous automated approaches. We implemented this method as a C++ tool and compared
+  it with three symbolic quantum circuit verifiers and two simulators on several benchmark
+  examples. The results show that our approach can solve problems with sizes orders
+  of magnitude larger than the state of the art.
+publication: '*Proceedings of the ACM on Programming Languages*'
+doi: 10.1145/3704868
+---
+POPL '25

content/publication/Amy2025/cite.bib

@@ -0,0 +1,20 @@
+@article{Amy2025,
+ title = {Linear and Non-linear Relational Analyses for Quantum Program Optimization},
+ author = {Amy, Matthew and Lunderville, Joseph},
+ year = {2025},
+ month = {January},
+ journal = {Proceedings of the ACM on Programming Languages},
+ publisher = {{Association for Computing Machinery}},
+ address = {New York, NY, USA},
+ volume = {9},
+ number = {POPL},
+ eid = {37},
+ pages = {37},
+ numpages = {32},
+ doi = {10.1145/3704873},
+ abstract = {The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program.    We show that the phase folding optimization can be re-cast as an affine relation analysis, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum programs with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for non-linear relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations — such as Clifford+t — we show that the sum-over-paths technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.},
+ keywords = {Quantum software, compiler optimization, data flow analysis, invariant generation, relational program analysis},
+ webnote = {POPL '25},
+ bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
+}
+

content/publication/Amy2025/index.md

@@ -0,0 +1,59 @@
+---
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: Linear and Non-linear Relational Analyses for Quantum Program Optimization
+subtitle: ''
+summary: ''
+authors:
+- Matthew Amy
+- Joseph Lunderville
+tags:
+- Quantum software
+- compiler optimization
+- data flow analysis
+- invariant generation
+- relational program analysis
+categories: []
+date: '2025-01-01'
+lastmod: 2025-08-20T07:44:17-05:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '2'
+abstract: The phase folding optimization is a circuit optimization used in many quantum
+  compilers as a fast and effective way of reducing the number of high-cost gates
+  in a quantum circuit. However, existing formulations of the optimization rely on
+  an exact, linear algebraic representation of the circuit, restricting the optimization
+  to being performed on straightline quantum circuits or basic blocks in a larger
+  quantum program.    We show that the phase folding optimization can be re-cast as
+  an affine relation analysis, which allows the direct application of classical techniques
+  for affine relations to extend phase folding to quantum programs with arbitrarily
+  complicated classical control flow including nested loops and procedure calls. Through
+  the lens of relational analysis, we show that the optimization can be powered-up
+  by substituting other classical relational domains, particularly ones for non-linear
+  relations which are useful in analyzing circuits involving classical arithmetic.
+  To increase the precision of our analysis and infer non-linear relations from gate
+  sets involving only linear operations — such as Clifford+t — we show that the sum-over-paths
+  technique can be used to extract precise symbolic transition relations for straightline
+  circuits. Our experiments show that our methods are able to generate and use non-trivial
+  loop invariants for quantum program optimization, as well as achieve some optimizations
+  of common circuits which were previously attainable only by hand.
+publication: '*Proceedings of the ACM on Programming Languages*'
+doi: 10.1145/3704873
+---
+POPL '25

content/publication/Buckley2024/cite.bib

@@ -0,0 +1,20 @@
+@article{Buckley2024,
+ title = {An Algebraic Language for Specifying Quantum Networks},
+ author = {Buckley, Anita and Chuprikov, Pavel and Otoni, Rodrigo and Soul\'{e}, Robert and Rand, Robert and Eugster, Patrick},
+ year = {2024},
+ month = {June},
+ journal = {Proceedings of the ACM on Programming Languages},
+ publisher = {{Association for Computing Machinery}},
+ address = {New York, NY, USA},
+ volume = {8},
+ number = {PLDI},
+ eid = {200},
+ pages = {200},
+ numpages = {23},
+ doi = {10.1145/3656430},
+ abstract = {Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational semantics. BellKAT's constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.},
+ keywords = {Kleene algebra, quantum networks, entanglement},
+ webnote = {PLDI '24},
+ bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
+}
+

content/publication/Buckley2024/index.md

@@ -0,0 +1,57 @@
+---
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: An Algebraic Language for Specifying Quantum Networks
+subtitle: ''
+summary: ''
+authors:
+- Anita Buckley
+- Pavel Chuprikov
+- Rodrigo Otoni
+- Robert Soul'e
+- Robert Rand
+- Patrick Eugster
+tags:
+- Kleene algebra
+- quantum networks
+- entanglement
+categories: []
+date: '2024-06-01'
+lastmod: 2025-08-20T07:44:17-05:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '2'
+abstract: Quantum networks connect quantum capable nodes in order to achieve capabilities
+  that are impossible only using classical information. Their fundamental unit of
+  communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately,
+  Bell pairs are fragile and difficult to transmit directly, necessitating a network
+  of repeaters, along with software and hardware that can ensure the desired results.
+  Challenging intrinsic features of quantum networks, such as dealing with resource
+  competition, motivate formal reasoning about quantum network protocols. To this
+  end, we developed BellKAT, a novel specification language for quantum networks based
+  upon Kleene algebra. To cater to the specific needs of quantum networks, we designed
+  an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational
+  semantics. BellKAT's constructs describe entanglement distribution rules that allow
+  for modular specification. We give BellKAT a sound and complete equational theory,
+  allowing us to verify network protocols. We provide a prototype tool to showcase
+  the expressiveness of BellKAT and how to optimize and verify networks in practice.
+publication: '*Proceedings of the ACM on Programming Languages*'
+doi: 10.1145/3656430
+---
+PLDI '24

content/publication/Cao2025/cite.bib

@@ -0,0 +1,20 @@
+@article{Cao2025,
+ title = {MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum Simulation},
+ author = {Cao, Xiuqi and Zhou, Junyu and Liu, Yuhao and Shi, Yunong and Li, Gushu},
+ year = {2025},
+ month = {June},
+ journal = {Proceedings of the ACM on Programming Languages},
+ publisher = {{Association for Computing Machinery}},
+ address = {New York, NY, USA},
+ volume = {9},
+ number = {PLDI},
+ eid = {170},
+ pages = {170},
+ numpages = {25},
+ doi = {10.1145/3729269},
+ abstract = {Quantum Hamiltonian simulation, fundamental in quantum algorithm design, extends far beyond its foundational roots, powering diverse quantum computing applications. However, optimizing the compilation of quantum Hamiltonian simulation poses significant challenges. Existing approaches fall short in reconciling deterministic and randomized compilation, lack appropriate intermediate representations, and struggle to guarantee correctness. Addressing these challenges, we present MarQSim, a novel compilation framework. MarQSim leverages a Markov chain-based approach, encapsulated in the Hamiltonian Term Transition Graph, adeptly reconciling deterministic and randomized compilation benefits. Furthermore, we formulate a Minimum-Cost Flow model that can tune transition matrices to enforce correctness while accommodating various optimization objectives. Experimental results demonstrate MarQSim's superiority in generating more efficient quantum circuits for simulating various quantum Hamiltonians while maintaining precision.},
+ keywords = {Hamiltonian Simulation, Markov Chain, Minimum-Cost Flow Model, Quantum Computing},
+ webnote = {PLDI '25},
+ bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
+}
+

content/publication/Cao2025/index.md

@@ -0,0 +1,57 @@
+---
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: 'MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for
+  Quantum Simulation'
+subtitle: ''
+summary: ''
+authors:
+- Xiuqi Cao
+- Junyu Zhou
+- Yuhao Liu
+- Yunong Shi
+- Gushu Li
+tags:
+- Hamiltonian Simulation
+- Markov Chain
+- Minimum-Cost Flow Model
+- Quantum Computing
+categories: []
+date: '2025-06-01'
+lastmod: 2025-08-20T07:44:17-05:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '2'
+abstract: Quantum Hamiltonian simulation, fundamental in quantum algorithm design,
+  extends far beyond its foundational roots, powering diverse quantum computing applications.
+  However, optimizing the compilation of quantum Hamiltonian simulation poses significant
+  challenges. Existing approaches fall short in reconciling deterministic and randomized
+  compilation, lack appropriate intermediate representations, and struggle to guarantee
+  correctness. Addressing these challenges, we present MarQSim, a novel compilation
+  framework. MarQSim leverages a Markov chain-based approach, encapsulated in the
+  Hamiltonian Term Transition Graph, adeptly reconciling deterministic and randomized
+  compilation benefits. Furthermore, we formulate a Minimum-Cost Flow model that can
+  tune transition matrices to enforce correctness while accommodating various optimization
+  objectives. Experimental results demonstrate MarQSim's superiority in generating
+  more efficient quantum circuits for simulating various quantum Hamiltonians while
+  maintaining precision.
+publication: '*Proceedings of the ACM on Programming Languages*'
+doi: 10.1145/3729269
+---
+PLDI '25

content/publication/Carette2025/cite.bib

@@ -0,0 +1,20 @@
+@article{Carette2025,
+ title = {How to Bake a Quantum Π},
+ author = {Carette, Jacques and Heunen, Chris and Kaarsgaard, Robin and Sabry, Amr},
+ year = {2024},
+ month = {August},
+ journal = {Proceedings of the ACM on Programming Languages},
+ publisher = {{Association for Computing Machinery}},
+ address = {New York, NY, USA},
+ volume = {8},
+ number = {ICFP},
+ eid = {236},
+ pages = {236},
+ numpages = {29},
+ doi = {10.1145/3674625},
+ abstract = {We construct a computationally universal quantum programming language QuantumΠ from two copies of Π, the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is "rotated" by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.},
+ keywords = {quantum programming language, reversible computing, rig category, unitary quantum computing},
+ webnote = {ICFP '24},
+ bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
+}
+