Commit 94a74396 authored by Rene Thiemann's avatar Rene Thiemann
Browse files

sitegen, new topics for quantum compution/information

parent 65d5538f1b4b
......@@ -9906,3 +9906,20 @@ abstract =
used for type-safe conversions between the SI system and others, like
the British Imperial System (BIS).
 
[Isabelle_Marries_Dirac]
title = Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
author = Anthony Bordg <mailto:apdb3@cam.ac.uk>, Hanna Lachnitt<mailto:lachnitt@stanford.edu>, Yijun He<mailto:yh403@cam.ac.uk>
topic = Computer science/Algorithms/Quantum computing, Mathematics/Physics/Quantum information
date = 2020-11-22
notify = apdb3@cam.ac.uk, lachnitt@stanford.edu
abstract =
This work is an effort to formalise some quantum algorithms and
results in quantum information theory. Formal methods being critical
for the safety and security of algorithms and protocols, we foresee
their widespread use for quantum computing in the future. We have
developed a large library for quantum computing in Isabelle based on a
matrix representation for quantum circuits, successfully formalising
the no-cloning theorem, quantum teleportation, Deutsch's
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's
Dilemma.
......@@ -10,6 +10,7 @@ Computer science
Approximation
Mathematical
Optimization
Quantum computing
Concurrency
Process calculi
Data structures
......@@ -59,5 +60,6 @@ Mathematics
Combinatorics
Category theory
Physics
Quantum information
Misc
Tools
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">I</font>sabelle
<font class="first">M</font>arries
<font class="first">D</font>irac:
a
<font class="first">L</font>ibrary
for
<font class="first">Q</font>uantum
<font class="first">C</font>omputation
and
<font class="first">Q</font>uantum
<font class="first">I</font>nformation
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
Anthony Bordg (apdb3 /at/ cam /dot/ ac /dot/ uk),
Hanna Lachnitt (lachnitt /at/ stanford /dot/ edu) and
Yijun He (yh403 /at/ cam /dot/ ac /dot/ uk)
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2020-11-22</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
This work is an effort to formalise some quantum algorithms and
results in quantum information theory. Formal methods being critical
for the safety and security of algorithms and protocols, we foresee
their widespread use for quantum computing in the future. We have
developed a large library for quantum computing in Isabelle based on a
matrix representation for quantum circuits, successfully formalising
the no-cloning theorem, quantum teleportation, Deutsch's
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's
Dilemma.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Isabelle_Marries_Dirac-AFP,
author = {Anthony Bordg and Hanna Lachnitt and Yijun He},
title = {Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information},
journal = {Archive of Formal Proofs},
month = nov,
year = 2020,
note = {\url{http://isa-afp.org/entries/Isabelle_Marries_Dirac.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Jordan_Normal_Form.html">Jordan_Normal_Form</a>, <a href="Matrix_Tensor.html">Matrix_Tensor</a>, <a href="VectorSpace.html">VectorSpace</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Isabelle_Marries_Dirac/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Isabelle_Marries_Dirac/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Isabelle_Marries_Dirac/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Isabelle_Marries_Dirac-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -169,7 +169,7 @@ All the results have been applied to improve CeTA, our certifier to validate ter
<td class="data"><a href="Polynomial_Factorization.html">Polynomial_Factorization</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a>, <a href="Farkas.html">Farkas</a>, <a href="Groebner_Bases.html">Groebner_Bases</a>, <a href="Linear_Programming.html">Linear_Programming</a>, <a href="Perron_Frobenius.html">Perron_Frobenius</a>, <a href="QHLProver.html">QHLProver</a>, <a href="Stochastic_Matrices.html">Stochastic_Matrices</a>, <a href="Subresultants.html">Subresultants</a> </td></tr>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a>, <a href="Farkas.html">Farkas</a>, <a href="Groebner_Bases.html">Groebner_Bases</a>, <a href="Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a>, <a href="Linear_Programming.html">Linear_Programming</a>, <a href="Perron_Frobenius.html">Perron_Frobenius</a>, <a href="QHLProver.html">QHLProver</a>, <a href="Stochastic_Matrices.html">Stochastic_Matrices</a>, <a href="Subresultants.html">Subresultants</a> </td></tr>
......
......@@ -101,7 +101,7 @@ MathJax = {
Author:
</td>
<td class="data">
<a href="https://sites.google.com/site/anthonybordg/">Anthony Bordg</a>
Anthony Bordg (apdb3 /at/ cam /dot/ ac /dot/ uk)
</td>
</tr>
......
......@@ -142,7 +142,7 @@ property.</td>
<td class="data"><a href="Matrix.html">Matrix</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Knot_Theory.html">Knot_Theory</a> </td></tr>
<td class="data"><a href="Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a>, <a href="Knot_Theory.html">Knot_Theory</a> </td></tr>
......
......@@ -93,7 +93,7 @@ MathJax = {
Author:
</td>
<td class="data">
<a href="https://sites.google.com/site/anthonybordg/">Anthony Bordg</a>
Anthony Bordg (apdb3 /at/ cam /dot/ ac /dot/ uk)
</td>
</tr>
......
......@@ -132,7 +132,7 @@ MathJax = {
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a> </td></tr>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a>, <a href="Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a> </td></tr>
......
......@@ -88,6 +88,16 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td class="head">2020</td>
</tr>
<tr>
<td class="entry">
2020-11-22: <a href="entries/Isabelle_Marries_Dirac.html">Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information</a>
<br>
Authors:
Anthony Bordg,
Hanna Lachnitt
and Yijun He
</td>
</tr>
<tr>
<td class="entry">
2020-10-29: <a href="entries/Verified_SAT_Based_AI_Planning.html">Verified SAT-Based AI Planning</a>
......@@ -1351,7 +1361,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
2018-06-14: <a href="entries/Projective_Geometry.html">Projective Geometry</a>
<br>
Author:
<a href="https://sites.google.com/site/anthonybordg/">Anthony Bordg</a>
Anthony Bordg
</td>
</tr>
<tr>
......@@ -1359,7 +1369,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
2018-06-14: <a href="entries/Localization_Ring.html">The Localization of a Commutative Ring</a>
<br>
Author:
<a href="https://sites.google.com/site/anthonybordg/">Anthony Bordg</a>
Anthony Bordg
</td>
</tr>
<tr>
......
......@@ -9,7 +9,24 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>29 Oct 2020 00:00:00 +0000</pubDate>
<pubDate>22 Nov 2020 00:00:00 +0000</pubDate>
<item>
<title>Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information</title>
<link>https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html</link>
<guid>https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html</guid>
<dc:creator> Anthony Bordg, Hanna Lachnitt, Yijun He </dc:creator>
<pubDate>22 Nov 2020 00:00:00 +0000</pubDate>
<description>
This work is an effort to formalise some quantum algorithms and
results in quantum information theory. Formal methods being critical
for the safety and security of algorithms and protocols, we foresee
their widespread use for quantum computing in the future. We have
developed a large library for quantum computing in Isabelle based on a
matrix representation for quantum circuits, successfully formalising
the no-cloning theorem, quantum teleportation, Deutsch&#39;s
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner&#39;s
Dilemma.</description>
</item>
<item>
<title>Verified SAT-Based AI Planning</title>
<link>https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html</link>
......@@ -578,19 +595,5 @@ Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of ZFC, we construct a proper generic extension and
show that the latter also satisfies ZFC.</description>
</item>
<item>
<title>Banach-Steinhaus Theorem</title>
<link>https://www.isa-afp.org/entries/Banach_Steinhaus.html</link>
<guid>https://www.isa-afp.org/entries/Banach_Steinhaus.html</guid>
<dc:creator> Dominique Unruh, Jose Manuel Rodriguez Caballero </dc:creator>
<pubDate>02 May 2020 00:00:00 +0000</pubDate>
<description>
We formalize in Isabelle/HOL a result
due to S. Banach and H. Steinhaus known as
the Banach-Steinhaus theorem or Uniform boundedness principle: a
pointwise-bounded family of continuous linear operators from a Banach
space to a normed space is uniformly bounded. Our approach is an
adaptation to Isabelle/HOL of a proof due to A. Sokal.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -210,6 +210,8 @@
<a href="entries/Safe_Distance.html">Safe_Distance</a> &nbsp;
<strong>Optimization:</strong>
<a href="entries/Simplex.html">Simplex</a> &nbsp;
<strong>Quantum computing:</strong>
<a href="entries/Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a> &nbsp;
</div>
<h3>Concurrency</h3>
<div class="list">
......@@ -877,7 +879,9 @@
<a href="entries/No_FTL_observers.html">No_FTL_observers</a> &nbsp;
<a href="entries/Safe_Distance.html">Safe_Distance</a> &nbsp;
<a href="entries/Physical_Quantities.html">Physical_Quantities</a> &nbsp;
</div>
<strong>Quantum information:</strong>
<a href="entries/Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a> &nbsp;
</div>
<h3>Misc</h3>
<div class="list">
<a href="entries/FunWithFunctions.html">FunWithFunctions</a> &nbsp;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment