Search Results

Documents authored by Garrigue, Jacques

Artifact
Software
DOI: 10.4230/artifacts.22446
QECC: Quantum Computation and Error-Correcting Codes

Authors: Jacques Garrigue and Takafumi Saikawa

Abstract
Cite as

Jacques Garrigue, Takafumi Saikawa. QECC: Quantum Computation and Error-Correcting Codes (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22446,
   title = {{QECC: Quantum Computation and Error-Correcting Codes}}, 
   author = {Garrigue, Jacques and Saikawa, Takafumi},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:d4d158675180ee276e730bd7f67a9122a6472eb3;origin=https://github.com/t6s/qecc;visit=swh:1:snp:98c582f9ca38ec1ef707cc25a4ef8f23befe0386;anchor=swh:1:rev:afc45f0ce1b3258fbf0c9469085ff8749de14a2a}{\texttt{swh:1:dir:d4d158675180ee276e730bd7f67a9122a6472eb3}} (visited on 2024-11-28)},
   url = {https://github.com/t6s/qecc},
   doi = {10.4230/artifacts.22446},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.15
Typed Compositional Quantum Computation with Lenses

Authors: Jacques Garrigue and Takafumi Saikawa

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows one to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.
Cite as

Jacques Garrigue and Takafumi Saikawa. Typed Compositional Quantum Computation with Lenses. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garrigue_et_al:LIPIcs.ITP.2024.15,
  author =	{Garrigue, Jacques and Saikawa, Takafumi},
  title =	{{Typed Compositional Quantum Computation with Lenses}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.15},
  URN =		{urn:nbn:de:0030-drops-207431},
  doi =		{10.4230/LIPIcs.ITP.2024.15},
  annote =	{Keywords: quantum programming, semantics, lens, currying, Coq, MathComp}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.5
Proving Tree Algorithms for Succinct Data Structures

Authors: Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.
Cite as

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2019.5,
  author =	{Affeldt, Reynald and Garrigue, Jacques and Qi, Xuanrui and Tanaka, Kazunari},
  title =	{{Proving Tree Algorithms for Succinct Data Structures}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.5},
  URN =		{urn:nbn:de:0030-drops-110609},
  doi =		{10.4230/LIPIcs.ITP.2019.5},
  annote =	{Keywords: Coq, small-scale reflection, succinct data structures, LOUDS, bit vectors, self balancing trees}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact