forked from rnrand/group-site
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpublications.bib
199 lines (180 loc) · 10.8 KB
/
publications.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
@inproceedings{singhal2020verified,
title={Verified translation between low-level quantum languages},
author={Singhal, Kartik and Rand, Robert and Hicks, Michael},
booktitle={The First International Workshop on Programming Languages for Quantum Computing (PLanQC 2020)},
year={2020}
}
@inproceedings{hietala2020tracking,
title={Tracking Errors through Types in Quantum Programs},
author={Hietala, Kesha and Rand, Robert and Hicks, Michael},
booktitle={The First International Workshop on Programming Languages for Quantum Computing (PLanQC 2020)},
year={2020}
}
@inproceedings{rand2020gottesman,
title={Gottesman Types for Quantum Programs},
author={Rand, Robert and Sundaram, Aarthi and Singhal, Kartik and Lackey, Brad},
booktitle={Proceedings of the 17th International Conference on Quantum Physics and Logic, QPL},
volume={20},
year={2020}
}
@inproceedings{hietala2021verified,
title={A verified optimizer for quantum circuits},
author={Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Wu, Xiaodi and Hicks, Michael},
booktitle={Proceedings of the ACM on Programming Languages},
volume={5},
number={POPL},
pages={1--29},
year={2021},
doi = {10.1145/3434318},
url = {https://doi.org/10.1145/3434318},
publisher={ACM New York, NY, USA}
}
@article{hietala2021proving,
author = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Li, Liyi and Hicks, Michael},
title = {{Proving Quantum Programs Correct}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {21:1--21:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13916},
URN = {urn:nbn:de:0030-drops-139160},
doi = {10.4230/LIPIcs.ITP.2021.21},
annote = {Keywords: Formal Verification, Quantum Computing, Proof Engineering}
}
@inproceedings{rand2021extending,
title={Extending Gottesman Types Beyond the Clifford Group},
author={Robert Rand and Aarthi Sundaram and Kartik Singhal and Brad Lackey},
booktitle={The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021)},
year={2021}
}
@misc{marshall2021toward,
title = {Toward Formalizing the Q\# Programming Language},
author = {Marshall, Sarah and Singhal, Kartik and Hietala, Kesha and Rand, Robert},
year = {2021},
month = 5,
howpublished = {18th International Conference on Quantum Physics and Logic 2021},
url = {https://ks.cs.uchicago.edu/publication/tfqpl/},
abstract = {Q\# is a high-level programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its interpretation. We aim to provide a formal specification and semantics for Q\#, placing the language on a solid mathematical foundation, enabling further evolution of its design and type system, and leading to research in program correctness and verified compiler implementation. This poster describes our current progress and outlines the next steps.},
keywords = {quantum computing, quantum computation, programming languages, formal specification, formal language definitions, type systems, semantics and reasoning, quantum programming languages, language design, q\#},
note = {Extended abstract accepted to QPL 2021 for the Poster Session.}
}
@inproceedings{singhal2021toward,
title={Toward a Type-Theoretic Interpretation of Q#},
author={Kartik Singhal and Sarah Marshall and Kesha Hietala and Robert Rand},
booktitle={The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021)},
year={2021}
}
@inproceedings{hietala2021expanding,
title={Expanding the VOQC Toolkit},
author={Kesha Hietala and Liyi Li and Akshaj Gaur and Aaron Green and Robert Rand and Xiaodi Wu and Michael Hicks},
booktitle={The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021)},
year={2021}
}
@inproceedings{singhal2022qsharp,
title = {{Q\# as a Quantum Algorithmic Language}},
author = {Singhal, Kartik and Hietala, Kesha and Marshall, Sarah and Rand, Robert},
year = {2022},
month = {June},
booktitle = {Proceedings of the 19th International Conference on Quantum Physics and Logic (QPL 2022)},
archiveprefix = {arXiv},
eprint = {2206.03532}
}
@misc{sundaram2022rich,
archiveprefix = {arXiv},
author = {Aarthi Sundaram and Robert Rand and Kartik Singhal and Brad Lackey},
title = {A Rich Type System for Quantum Programs},
eprint = {2101.08939},
primaryclass = {quant-ph},
doi = {arXiv.2101.08939},
year = {2022}
}
@inproceedings{voichick2022qunity,
author = {Voichick, Finn and Li, Liyi and Rand, Robert and Hicks, Michael},
title = {Qunity: A Unified Language for Quantum and Classical Computing},
booktitle={Proceedings of the ACM on Programming Languages},
volume={5},
number={POPL},
year = {2023}
}
@misc{lehmann2022vyzx,
author = {Adrian Lehmann and Ben Caldwell and Robert Rand},
title = {{VyZX}: A Vision for Verifying the {ZX} Calculus},
archiveprefix = {arXiv},
doi = {10.48550/ARXIV.2205.05781},
url = {https://arxiv.org/abs/2205.05781},
eprint = {2205.05781},
primaryclass = {quant-ph},
year = {2022}
}
@inproceedings{zweifler2022quantumlib,
title={{QuantumLib: A Library for Quantum Computing in Coq}},
author={Jacob Zweifler and Kesha Hietala and Robert Rand},
booktitle={The Coq Workshop},
year={2022}
}
@inproceedings{hietala2022qstar,
title={Q*: Implementing Quantum Separation Logic in F*},
author={Kesha Hietala and Sarah Marshall and Robert Rand and Nikhil Swamy},
booktitle={The Third International Workshop on Programming Languages for Quantum Computing (PLanQC 2022)},
year={2022}
}
@article{demicheli2022,
author={De Micheli, Giovanni and Jiang, Jie-Hong R. and Rand, Robert and Smith, Kaitlin and Soeken, Mathias},
journal={IEEE Journal on Emerging and Selected Topics in Circuits and Systems},
title={Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective},
year={2022},
doi={10.1109/JETCAS.2022.3205174}
}
@misc{singhal2022separation,
title = {Beyond Separation: Toward a Specification Language for Modular Reasoning about Quantum Programs},
author = {Kartik Singhal and Robert Rand and Matthew Amy},
year = {2022},
howpublished = {Programming Languages for Quantum Computing (PLanQC 2022) Poster Session},
note = {Extended abstract accepted to PLanQC 2022 for the Poster Session.}
}
@article{peng2023shor,
author = {Yuxiang Peng and Kesha Hietala and Runzhou Tao and Liyi Li and Robert Rand and Michael Hicks and Xiaodi Wu },
title = {A formally certified end-to-end implementation of Shor’s factorization algorithm},
journal = {Proceedings of the National Academy of Sciences},
volume = {120},
number = {21},
pages = {e2218775120},
year = {2023},
doi = {10.1073/pnas.2218775120},
URL = {https://www.pnas.org/doi/abs/10.1073/pnas.2218775120},
eprint = {https://www.pnas.org/doi/pdf/10.1073/pnas.2218775120},
abstract = {Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof’s validity is automatically confirmed—certified—by a “proof assistant.” Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.}
}
@inproceedings{buckley2023towards,
author = {Buckley, Anita and Chuprikov, Pavel and Otoni, Rodrigo and Rand, Robert and Soul\'{e}, Robert and Eugster, Patrick},
title = {Towards an Algebraic Specification of Quantum Networks},
year = {2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3610251.3610557},
doi = {10.1145/3610251.3610557},
abstract = {The main attributes of quantum networks are the utilization of quantum phenomena, security guarantees, and availability of their main quantum resource - entanglement. The fundamental differences between classical and quantum information will require joint efforts in physics, engineering and computer science to make quantum networks functional and scalable. A common language must be established between the hardware and software community. We envision a foundational model for quantum network programming languages. Such a model should contain the essential constructs for programming quantum networks, allow for specification and verification of end-to-end entanglement distribution, and provide guidelines for composing network protocols.},
booktitle = {Proceedings of the 1st Workshop on Quantum Networks and Distributed Quantum Computing},
pages = {7–12},
numpages = {6},
keywords = {entanglement, kleene algebra, quantum networks},
location = {New York, NY, USA},
series = {QuNet '23}
}
@INPROCEEDINGS{evans2023,
author={Evans, Aidan and Omonije, Seun and Soulé, Robert and Rand, Robert},
booktitle={2023 IEEE/ACM 4th International Workshop on Quantum Software Engineering (Q-SE)},
title={MCBeth: A Measurement-based Quantum Programming Language},
year={2023},
volume={},
number={},
pages={1-8},
keywords={Computer languages;Adaptation models;Quantum computing;Current measurement;Computational modeling;Logic gates;Programming;quantum computing;programming languages;measurement-based quantum computing;one-way quantum computer;distributed computing},
doi={10.1109/Q-SE59154.2023.00007}
}