Quantum coin flipping is a cryptographic primitive in which two or more parties that do not trust each other want establish a fair coin flip. These parties are not physically near each other and use quantum communication channels to interact. A quality of protocols is measured by the best possible cheating strategy, which is the solution of a complex semidefinite optimization problem. In this master thesis we show new explicit bounds in multiparty quantum coin flipping, we investigate how to explicitly formulate these problem in a standard form, we show that a fair coin flip results in the lowest possible bias and we determine more measures of the quality of a protocol. Furthermore, this master thesis presents a rigorous and detailed mathematical description of semidefinite optimization, quantum information theory and quantum coin flipping. This thesis also includes an article written together with J. Mulderij, T. Attema, I. Chiscop and F. Phillipson on distributed quantum computing. In this article, we pose new questions and formulate integer linear programs that solve to find optimal assignment of qubits to computers for a given network of quantum computers and quantum algorithm.

Session types are a formal method to describe communication protocols between two or more actors. Protocols that type check are guaranteed to respect communication safety, linearity, progress, and session fidelity. Basic session types, however, do not in general guarantee anything about the contents of messages, while real-life applications of structured communication, such as money transfers at the ING bank, could benefit greatly from content safety. In this work, we show how to state, verify, and run session-typed protocols with dependent variables in Idris, using Idris’ ST library.
We also present an extension to the protocol description language Scribble. Scribble is a language for defining high-level global protocols between multiple actors and comes with a tool that automatically generates type signatures of local protocols for each actor in Java, in a way that these type signatures ensure that local actors follow the global protocol specification. We describe a new variant of the Scribble language which adds support for dependent variables, and a new tool for automatically generating Idris type signatures of local protocols for actors in a way that enforces dependent invariants.