2 Search Results for "de Felice, Giovanni"

Document

DOI: 10.4230/LIPIcs.FSCD.2024.30

homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

Authors: Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

Cite as

Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30,
  author =	{Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie},
  title =	{{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{30:1--30:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.30},
  URN =		{urn:nbn:de:0030-drops-203594},
  doi =		{10.4230/LIPIcs.FSCD.2024.30},
  annote =	{Keywords: Higher category theory, proof assistant, string diagrams}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2018.17

A Diagrammatic Axiomatisation of Fermionic Quantum Circuits

Authors: Amar Hadzihasanovic, Giovanni de Felice, and Kang Feng Ng

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract

We introduce the fermionic ZW calculus, a string-diagrammatic language for fermionic quantum computing (FQC). After defining a fermionic circuit model, we present the basic components of the calculus, together with their interpretation, and show how the main physical gates of interest in FQC can be represented in the language. We then list our axioms, and derive some additional equations. We prove that the axioms provide a complete equational axiomatisation of the monoidal category whose objects are quantum systems of finitely many local fermionic modes, with operations that preserve or reverse the parity (number of particles mod 2) of states, and the tensor product, corresponding to the composition of two systems, as monoidal product. We achieve this through a procedure that rewrites any diagram in a normal form. We conclude by showing, as an example, how the statistics of a fermionic Mach-Zehnder interferometer can be calculated in the diagrammatic language.

Cite as

Amar Hadzihasanovic, Giovanni de Felice, and Kang Feng Ng. A Diagrammatic Axiomatisation of Fermionic Quantum Circuits. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{hadzihasanovic_et_al:LIPIcs.FSCD.2018.17,
  author =	{Hadzihasanovic, Amar and de Felice, Giovanni and Ng, Kang Feng},
  title =	{{A Diagrammatic Axiomatisation of Fermionic Quantum Circuits}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.17},
  URN =		{urn:nbn:de:0030-drops-91873},
  doi =		{10.4230/LIPIcs.FSCD.2018.17},
  annote =	{Keywords: Fermionic Quantum Computing, String Diagrams, Categorical Quantum Mechanics}
}

Refine by Author
1 Corbyn, Nathan
1 Hadzihasanovic, Amar
1 Heidemann, Lukas
1 Hu, Nick
1 Ng, Kang Feng
Show More...

Refine by Classification
1 Software and its engineering → Software notations and tools
1 Theory of computation → Quantum computation theory

Refine by Keyword
1 Categorical Quantum Mechanics
1 Fermionic Quantum Computing
1 Higher category theory
1 String Diagrams
1 proof assistant
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2018
1 2024