Search Results

Documents authored by Saikawa, Takafumi

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
Short Paper
DOI: 10.4230/LIPIcs.ITP.2024.39
Robust Mean Estimation by All Means (Short Paper)

Authors: Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann

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

Abstract
We report the results of a verification experiment on an algorithm for robust mean estimation, i.e., an algorithm that computes a mean in the presence of outliers. We formalize the algorithm in the Coq proof assistant and devise a pragmatic approach for identifying and solving issues related to the choice of bounds. To keep our formalization succinct and generic, we recast the original argument using an existing library for finite probabilities that we extend with reusable lemmas. To formalize the original algorithm, which relies on a subtle convergence argument, we observe that by adding suitable termination checks, we can turn it into a well-founded recursion without losing its original properties. We also exploit a tactic for solving real-valued inequalities by approximation to heuristically fix inaccurate constant values in the original proof.
Cite as

Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann. Robust Mean Estimation by All Means (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 39:1-39:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.39,
  author =	{Affeldt, Reynald and Barrett, Clark and Bruni, Alessandro and Daukantas, Ieva and Khan, Harun and Saikawa, Takafumi and Sch\"{u}rmann, Carsten},
  title =	{{Robust Mean Estimation by All Means}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{39:1--39:8},
  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.39},
  URN =		{urn:nbn:de:0030-drops-207679},
  doi =		{10.4230/LIPIcs.ITP.2024.39},
  annote =	{Keywords: robust statistics, probability theory, formal verification}
}
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