Séminaire le 4 décembre 2008

I'll describe an ongoing project on formalizing (constructive) domain theory and denotational semantics of programming languages in Coq. This currently goes as far as the proof of adequacy for a semantics of an untyped CBV language in a recursively-defined domain, and is joint work with Andrew Kennedy and Carsten Varming.

We will provide a short introduction to classical and quantum interactive proofs and describe some of the main results and open questions. In an interactive proof system, an all-powerful prover and an efficient verifier receive an instance of a problem and the prover is trying to convince the verifier that it is a YES instance by exchanging messages (e.g. is there a hamiltonian cycle in this graph, is the permanent of this matrix 0). Such a system is complete and sound if the verifier accepts with high probability when it is a YES instance and rejects with high probability when it is a NO instance. In the quantum world, we allow the communication to be quantum and the main question we ask is whether such systems are more powerful or not. We will discuss the properties of such systems and their relation to the classical ones. Moreover, we will discuss a special case of interative proofs, the Zero Knowledge Proof systems both in the classical and the quantum world. No prior knowledge of quantum computing will be assumed.

Extraits du "Pavé": Une théorie des jeux, crédibilités, plausibilités, et prévisions dans un cadre topologique.