Hi! Today I will write about boring “computer science” stuff!
Just joking, it is not boring at all and I will try to keep it as simple as possible -I can just hear my best friends laughing at this statement, because every time I say something like “it is easy to see” or “as simple as possible” then it happens that a huge wicked formula appears, but it is not my fault 🙂 I can’t help it.
Ok, are you ready? Let’s start.

Last month I attended a workshop on Reversibility and product-forms in Markov Chains at the Ca’ Foscari University in Venice and I presented the Entangλe framework.
You can find the slides here.

What is Entangλe?
In the about me I wrote that I am currently working on model checking of quantum protocols so… this is one of my first output as a part of my Ph.D project.
To be completely honest I worked on it with my friend and, I hope, perspective talented colleague Leonardo and with my supervisors.

Anyways, Entangλe is a framework that links together Quipper , a programming language that wants to simplify the art of programming quantum protocols and QPMC , a model checker for quantum protocols. I will not focus here on the details of model checking or quantum programming, I prefer to post a very basic tutorial about them in the future.
Why have we decided to bridge these tools? But of course, because of the lack of a unique framework allowing, on the one hand the programming and the simulation of quantum programs and on the other their formal verification.
Entangλe needs some optimisation but it is fully working, even if a bit essential by now. You may find it on Github . It takes as input Quipper code and gives in output a QPMC model.

Let’s see an easy example. One of the first algorithms we have tested is the famous Grover’s Database Search. Schematic circuit for Grover’s Database Search 1

The aim of Grover’s algorithm is that of searching for the index x of an element in a N-dimensional unstructured space. We assume N = 2n, so that the indexes are represented by n-bit strings.

The algorithm solves the problem by considering a function f : {0, 1}n → {0, 1} such that f(x) = 1 if and only if x is a solution. This problem can be solved by a quantum computer more efficiently than by a classical one (even if the speedup is not astonishing in this case).

Anyway in a short tutorial I will show a better description of quantum algorithms. Let’s now focus on Entangλe.

For the experiment we decided to use a search space of size N = 4 with the oracle returning the string x = 3, i.e. in this case the oracle is a cc-not gate and the circuit looks like this: Grover ‘s algorithm for N=4 search space 2

How do we make it work with Entangλe? Ok, be sure to download it from Github . First of all you must install Quipper ! You can find all the essentials here in the Downloading-Installing sections.
Second, enter the entangle folder you have downloaded and open the Main.hs file, located in the src folder.

In the examples section of the Main.hs file you can type an example program, in this case will be our implementation of the Grover’s algorithm but you can also try something else!

```grover_naive :: (Qubit, Qubit, Qubit) -> Circ (Bit, Bit)
grover_naive (q1,q2,q3) = do
qnot_at q3 `controlled` [q1, q2]
gate_X_at q1
gate_X_at q2
qnot_at q2 `controlled` q1
gate_X_at q1
gate_X_at q2
measure (q1,q2)```

Now, always in the Main.hs you have to modify the main putting after the full_out the name of the algorithm you want to translate into QPMC code:

``` main = do
full_out grover_naive```

Now is time to compile it. Open the Terminal and be sure to be in the src folder and type

`Lindas-MacBook-Air:src linda\$ quipper ./Main.hs `

.
Once compiled you can run it by typing

`Lindas-MacBook-Air:src linda\$ ./Main `

and you will have as a result the converted code.

Easy!

Now you can copy the generated code

```qmc
const matrix A1 = [...];
.
. // I have shortened here because we are dealing with 8x8 matrices :)
.
const matrix A14 = [...];
module test
s: [0..14] init 0;
[] (s = 0) -> <> : (s' = 1);
[] (s = 1) -> <> : (s' = 2);
[] (s = 2) -> <> : (s' = 3);
[] (s = 3) -> <> : (s' = 4);
[] (s = 4) -> <> : (s' = 5);
[] (s = 5) -> <> : (s' = 6);
[] (s = 6) -> <> : (s' = 7);
[] (s = 7) -> <> : (s' = 8);
[] (s = 8) -> <> : (s' = 9) + <> : (s' = 10);
[] (s = 9) -> <> : (s' = 11) + <> : (s' = 12);
[] (s = 10) -> <> : (s' = 13) + <> : (s' = 14);
[] (s = 11) -> (s' = 11);
[] (s = 12) -> (s' = 12);
[] (s = 13) -> (s' = 13);
[] (s = 14) -> (s' = 14);
endmodule
```

and use it to test some interesting formulas using the QPMC model checker here! When you save the module be sure to use the prism-qmc model type or it will not work.

That’s it, for now. There are many open challenges and the code must be optimised so stay tuned and if you are interested remember, collaborations are always welcome 🙂