Jose Manuel Rodríguez Caballero (Jul 04 2019 at 20:36): Jose Manuel Rodríguez Caballero (Jul 04 2019 at 20:36):I defined an embedding from the "Isabelle Marries Dirac" library into the library of D. Unruh and myself. In this way, the finite-dimensional constructions, e.g., all the quantum algorithms, can be studied using the infinite-dimensional methods that we are implementing, in particular the Quantum Relational Hoare Logic. Here is the link: Finite_Dimensional_Case.thy
Last updated: Nov 21 2024 at 08:25 UTC