Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Quantum Numbers02:43

Quantum Numbers

45.1K
It is said that the energy of an electron in an atom is quantized; that is, it can be equal only to certain specific values and can jump from one energy level to another but not transition smoothly or stay between these levels.
45.1K
The Quantum-Mechanical Model of an Atom02:45

The Quantum-Mechanical Model of an Atom

53.0K
Shortly after de Broglie published his ideas that the electron in a hydrogen atom could be better thought of as being a circular standing wave instead of a particle moving in quantized circular orbits, Erwin Schrödinger extended de Broglie’s work by deriving what is now known as the Schrödinger equation. When Schrödinger applied his equation to hydrogen-like atoms, he was able to reproduce Bohr’s expression for the energy and, thus, the Rydberg formula governing hydrogen spectra.
53.0K
Parseval's Theorem01:18

Parseval's Theorem

728
Parseval's theorem is a fundamental concept in signal processing and harmonic analysis. It asserts that for a periodic function, the average power of the signal over one period equals the sum of the squared magnitudes of all its complex Fourier coefficients. This theorem, named after Marc-Antoine Parseval, provides a powerful tool for analyzing the energy distribution in signals.
Interestingly, Parseval's theorem also holds for the trigonometric form of the Fourier series, which...
728
Castigliano's Theorem01:18

Castigliano's Theorem

588
Castigliano's theorem analyzes displacements and rotations in elastic structures. It relates the derivative of elastic strain energy to the applied forces or moments, allowing for the calculation of deformations. The theorem states that the partial derivative of the total strain energy of a system with respect to a specific load results in the displacement at the point where the load is applied. This principle applies to both forces and moments.
588
Lattice Centering and Coordination Number02:33

Lattice Centering and Coordination Number

10.3K
The structure of a crystalline solid, whether a metal or not, is best described by considering its simplest repeating unit, which is referred to as its unit cell. The unit cell consists of lattice points that represent the locations of atoms or ions. The entire structure then consists of this unit cell repeating in three dimensions. The three different types of unit cells present in the cubic lattice are illustrated in Figure 1.
Types of Unit Cells
Imagine taking a large number of identical...
10.3K
Routh-Hurwitz Criterion II01:19

Routh-Hurwitz Criterion II

471
In the application of the Routh-Hurwitz criterion, two specific scenarios can arise that complicate stability analysis.
The first scenario occurs when a singular zero appears in the first column of the Routh table. This situation creates a division by zero issues. To resolve this, a small positive or negative number, denoted as epsilon (∈), is substituted for the zero. The stability analysis proceeds by assuming a sign for ∈. If ∈ is positive, any sign change in the first...
471

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

The association between the diabetes mellitus duration and the risk of pulmonary tuberculosis in the elderly: evidence from a community-based study in China.

Journal of global health·2026
Same author

The association between exposure to air pollutants and latent tuberculosis infection prevalence in the elderly population: a population-based cross-sectional study from China.

Journal of global health·2026
Same author

Elevated serum peroxiredoxin 1 is a biomarker of multiorgan failure in ARDS.

BMJ open respiratory research·2026
Same author

Peroxiredoxin 1 mediates bleomycin-induced acute lung injury in mice via macrophage NOD1/NF-κB axis.

Respiratory research·2026
Same author

Succinate-mediated activation of the GPR91/MALT1/NF-κB/CCL2 pathway in macrophages contributes to pulmonary fibrosis.

International immunopharmacology·2026
Same author

Corrigendum to "The association between pulmonary tuberculosis recurrence and exposure to fine particulate matter and residential greenness: A population-based retrospective study" has already been published in the issue [One Health, volume 20, article 101035].

One health (Amsterdam, Netherlands)·2026
Same journal

Combining Higher-Order Logic with Set Theory Formalizations.

Journal of automated reasoning·2023
Same journal

Synthesising Programs with Non-trivial Constants.

Journal of automated reasoning·2023
Same journal

Unifying Splitting.

Journal of automated reasoning·2023
Same journal

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.

Journal of automated reasoning·2023
Same journal

A Formalization of SQL with Nulls.

Journal of automated reasoning·2022
Same journal

A Comprehensive Framework for Saturation Theorem Proving.

Journal of automated reasoning·2022
See all related articles

Related Experiment Video

Updated: Oct 14, 2025

Scalable Quantum Integrated Circuits on Superconducting Two-Dimensional Electron Gas Platform
05:39

Scalable Quantum Integrated Circuits on Superconducting Two-Dimensional Electron Gas Platform

Published on: August 2, 2019

9.8K

Certified Quantum Computation in Isabelle/HOL.

Anthony Bordg1, Hanna Lachnitt2, Yijun He3

  • 1Department of Computer Science and Technology, University of Cambridge, Cambridge, UK.

Journal of Automated Reasoning
|November 1, 2021
PubMed
Summary
This summary is machine-generated.

Researchers are formalizing quantum algorithms and information theory using Isabelle/HOL. This work includes formalizing key quantum concepts and algorithms, paving the way for secure quantum computing.

Keywords:
CertificationDeutsch–Jozsa algorithmDeutsch’s algorithmIsabelle/HOLNo-cloningQuantum computingQuantum prisoner’s dilemmaQuantum teleportation

More Related Videos

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit
05:30

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit

Published on: September 8, 2023

733
Generation and Coherent Control of Pulsed Quantum Frequency Combs
06:42

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

9.2K

Related Experiment Videos

Last Updated: Oct 14, 2025

Scalable Quantum Integrated Circuits on Superconducting Two-Dimensional Electron Gas Platform
05:39

Scalable Quantum Integrated Circuits on Superconducting Two-Dimensional Electron Gas Platform

Published on: August 2, 2019

9.8K
Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit
05:30

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit

Published on: September 8, 2023

733
Generation and Coherent Control of Pulsed Quantum Frequency Combs
06:42

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

9.2K

Area of Science:

  • Computer Science
  • Quantum Information Theory
  • Formal Methods

Background:

  • Formal methods are crucial for algorithm and protocol safety and security.
  • The increasing complexity of quantum algorithms necessitates rigorous verification.
  • Quantum computing holds significant potential but requires robust foundational methods.

Purpose of the Study:

  • To formalize quantum algorithms and results in quantum information theory.
  • To develop a comprehensive library for quantum computing within the Isabelle/HOL proof assistant.
  • To explore the application of formal methods in quantum game theory.

Main Methods:

  • Utilizing the Isabelle/HOL proof assistant for formal verification.
  • Developing a matrix-based representation for quantum circuits.
  • Applying formal methods to established quantum algorithms and theorems.

Main Results:

  • Successfully formalized the no-cloning theorem, quantum teleportation, Deutsch's algorithm, and the Deutsch-Jozsa algorithm.
  • Developed a substantial library for quantum computing in Isabelle/HOL.
  • Investigated quantum game theory, including the quantum Prisoner's Dilemma.

Conclusions:

  • Formal methods are essential for the future of quantum computing.
  • The developed Isabelle/HOL library provides a robust framework for quantum algorithm verification.
  • This formalization effort contributes to the foundational understanding and secure development of quantum information technologies.