QuEnG Seminar || Quantum Computing - Projective Measurements and the CHSH inequality with Isabelle/HOL

on the April 28, 2021

At 2:00pm
The Quantum Computing seminars cover all aspects of quantum computing and quantum information theory, and will be jointly organised with the quantum information community in Lyon.
The next QuEnG Quantum Computing seminar will be given by Mnacho Echenim (LIG – Laboratoire d’Informatique de Grenoble) on Wednesday 28 April at 2pm on Zoom (link below). 
Title: Projective Measurements and the CHSH inequality with Isabelle/HOL
Abstract: Interactive theorem provers are tools that permit users to produce formal mathematical proofs. These tools have been used to guarantee that highly non-trivial proofs are indeed correct, and, in some cases, have permitted the detection of gaps in already published proofs. In this talk we investigate how interactive theorem provers can be used in the context of quantum computing, by formalizing fundamental notions from this domain. More precisely, we present a formalization of projective measurements in Isabelle/HOL, along with the formal construction of the projective measurement associated with a given observable. We also formalize local joint probability distributions and the CHSH inequality, which permits to prove that there is no local hidden-variable theory for quantum mechanics.
Zoom link + details:
Heure : 28 avr. 2021 02:00 PM Paris
Participer à la réunion Zoom
Published on April 26, 2021

Practical informations


Online (Zoom)