Abstract

This work consists of three parts: the original dissertation thesis proposal and two related published articles. Their titles and abstracts follow: ------------------------------- Title: Quantum programmning Abstract: Quantum computing is a young and promising branch of computer science. It uses the laws of quantum mechanics for speeding up various computations. However, mathematical models that physicists use for a description of quantum systems, are not practical for programming in the quantum world. For this reason, both purely quantum and combined classical-quantum programming languages are being developed. However, many of proposed imperative languages do not have well-defined semantics. Moreover, in real situations programs have to communicate. Therefore, a programming language should offer tools for interprocess communication. However, current quantum programming languages do not offer tools for interprocess communication. Nowadays, only quantum process algebras deal with the communication. The aim of the dissertation is to develop a higher-level imperative programming language for programming in both classical and quantum world. This language will be typed, will offer tools for interprocess communication and will have well-defined semantics. ------------------------------- Title: LanQ - an Imperative Quantum Programming Language Abstract: LanQ is an imperative high-level quantum programming language that allows combining of quantum and classical computations in the way of classical control, quantum data. Moreover, it offers tools for communication and parallel running of programs. In the paper, we introduce the language. ------------------------------- Title: Syntactic Type Soundness in Structured Imperative Languages Abstract: We present a general technique for proving type soundness of a structured imperative programming language. We show this technique on a simple language IPL. A program in the language is a set of functions. To prove type soundness we develop an approximate syntactic predicate that statically checks function correctness. The presented result is a byproduct of the development of a quantum programming language LanQ where it was used to prove type soundness. Nevertheless, it is applicable to a wide range of other existing classical languages. ------------------------------- …víceméně