Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Quantum Programming Language LanQ

Hynek Mlnařík

Published Jan 1, 2007• 9 citations
OpenAlex

Abstract

We define a typed imperative quantum programming language LanQ that allows programmers to implement any algorithm that is based on either one, or a combination of classical or quantum computation. The language syntax is similar to that of C language and forces programmers to structure their programs into smaller pieces of code (methods, blocks) what makes the program better readable and maintainable compared to programs in unstructured languages. It allows programmers to assign a quantum system to several variables in such a way that all quantum principles, namely no-cloning and no-deleting, are obeyed. The language also offers process algebraic features such as creation a new process (this is done by forking a new process from a running one) and interprocess communication. It therefore supports implementation of multiparty protocols. The resources sent over a channel are handled so that they are always owned by at most one process at one time. In the thesis, we formally describe the language syntax, its type system, memory model used and operational semantics. We also prove type soundness property for the noncommunicating part of the language and for the full language provided the programs are guaranteed to use only a well-formed communication.. We show an example run of a random number generator implemented in the language and provide a reference manual to the implementation of LanQ simulator which is publicly available at http://lanq.sf.net/.

Related papers

Operational Semantics and Type Soundness of Quantum Programming Language LanQ

Hynek Mlnařík

We present an imperative quantum programming language LanQ which was designed to support combination of quantum and classical programming and basic process operations - process creation and interprocess communication. The language can thus be used for implementing both classical and quantum algorithms and protocols. Its syntax is similar to that of C language what makes it easy to learn for existing programmers. In this paper, we present operational semantics of the language and a proof of type soundness of the noncommunicating part of the language. We provide an example run of a quantum random number generator.

arXiv:0708.0890•Aug 7, 2007•10 citations

SEMANTICS OF QUANTUM PROGRAMMING LANGUAGE LANQ

Hynek Mlnařík

We show a memory model of an imperative concurrent quantum programming language LanQ. The memory model is used to specify the shape of semantical structure upon which the language operational semantics is defined. We also outline the language abilities in the area of formal verification on an example implementation of teleportation protocol.

International Journal of Quantum Information•Jul 1, 2008•10 citations

LanQ - an Imperative Quantum Programming Language

Hynek Mlnařík

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.

•Jan 1, 2006•1 citation

Towards a quantum programming language

Peter Selinger

We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.

Mathematical Structures in Computer Science•Aug 1, 2004•478 citations

Communicating Quantum Processes

Simon J. Gay, Rajagopal Nagarajan

We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.

arXiv:quant-ph/0409052•Sep 9, 2004•5 citations

Communicating quantum processes

Simon J. Gay, Rajagopal Nagarajan

We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.

ACM SIGPLAN Notices•Jan 12, 2005•15 citations
We define a typed imperative quantum programming language LanQ that allows programmers to implement any algorithm that is based on either one, or a combination of classical or quantum computation. The language syntax is similar to that of C language and forces programmers to structure their programs into smaller pieces of code (methods, blocks) what makes the program better readable and maintainable compared to programs in unstructured languages. It allows programmers to assign a quantum system to several variables in such a way that all quantum principles, namely no-cloning and no-deleting, are obeyed. The language also offers process algebraic features such as creation a new process (this is done by forking a new process from a running one) and interprocess communication. It therefore supports implementation of multiparty protocols. The resources sent over a channel are handled so that they are always owned by at most one process at one time. In the thesis, we formally describe the language syntax, its type system, memory model used and operational semantics. We also prove type soundness property for the noncommunicating part of the language and for the full language provided the programs are guaranteed to use only a well-formed communication.. We show an example run of a random number generator implemented in the language and provide a reference manual to the implementation of LanQ simulator which is publicly available at http://lanq.sf.net/.
We present an imperative quantum programming language LanQ which was designed to support combination of quantum and classical programming and basic process operations - process creation and interprocess communication. The language can thus be used for implementing both classical and quantum algorithms and protocols. Its syntax is similar to that of C language what makes it easy to learn for existing programmers. In this paper, we present operational semantics of the language and a proof of type soundness of the noncommunicating part of the language. We provide an example run of a quantum random number generator.
We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.