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

arXiv:2204.03885 · Electronic Proceedings in Theoretical Computer Science

A Quick Overview on the Quantum Control Approach to the Lambda Calculus

Alejandro Díaz-Caro

Published Apr 7, 2022• 1 citation
arXivHTMLPDF

Abstract

In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrighi and Dowek's seminal work until today.

DOI
10.4204/eptcs.357.1

Related papers

A Lambda Calculus for Quantum Computation with Classical Control

Peter Selinger, Benoît Valiron

arXiv:cs/0404056•Lecture notes in computer science•Jan 1, 2005•34 citations

On quantum lambda calculi: a foundational perspective

Margherita Zorzi

In this paper, we propose an approach to quantum λ-calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus calledQ, we will study standard properties such as confluence and subject reduction, and some good quantum properties. We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator toQ. On the resulting calculus, calledQ*, we will propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.

Mathematical Structures in Computer Science•Nov 17, 2014•30 citations

FROM QUANTUM LOGIC TO QUANTUM COMPUTATIONAL LOGIC

Michele Caponigro, Stefano Mancini

We overview the main concepts of quantum logic ranging from the orthodox formulation to the quantum computational aspects.

•Jan 1, 2006•0 citations

Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits

Alejandro Díaz-Caro, Pablo J. Arrighi, Manuel Gadella +1 more

This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML [Grattage, J. and T. Altenkirch, A functional quantum programming language, in: LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258] or Lineal [Arrighi, P. and G. Dowek, A computational definition of the notion of vectorial space, Electronic Notes in Theoretical Computer Science 117 (2005), pp. 249–261; Arrighi, P. and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence, in: B. Buchberger, editor, Term Rewriting and Applications, 19th International Conference, RTA-08, To appear in LNCS (2008), eprint available at arXiv:quant-ph/0612199], which is the subject of further research.

arXiv:0806.2447•Electronic Notes in Theoretical Computer Science•Feb 1, 2011•15 citations

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We prove subject reduction, confluence and a standardization theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

arXiv:cs/0703152•Mar 30, 2007•0 citations

A fully abstract model for quantum controlled lambda calculus

Alejandro Díaz-Caro, Octavio Malherbe

•Jun 1, 2018•1 citation
In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrighi and Dowek's seminal work until today.
In this paper, we propose an approach to quantum λ-calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus calledQ, we will study standard properties such as confluence and subject reduction, and some good quantum properties. We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator toQ. On the resulting calculus, calledQ*, we will propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.
This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML [Grattage, J. and T. Altenkirch, A functional quantum programming language, in: LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258] or Lineal [Arrighi, P. and G. Dowek, A computational definition of the notion of vectorial space, Electronic Notes in Theoretical Computer Science 117 (2005), pp. 249–261; Arrighi, P. and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence, in: B. Buchberger, editor, Term Rewriting and Applications, 19th International Conference, RTA-08, To appear in LNCS (2008), eprint available at arXiv:quant-ph/0612199], which is the subject of further research.