2007/03/30 by Ugo Dal Lago, Lago, Ugo Dal, Andrea Masini +3
Computer Science · #Computability, Logic, AI Algorithms #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Quantum Computing Algorithms and Architecture #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0703152
25 pages
arxiv created 2007/03/30 · openalex publication_date 2007/03/30 · arxiv updated 2009/12/01 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
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.