Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power
<|reference_start|>Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power: 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.<|reference_end|>
@article{lago2007quantum,
    title={Quantum Lambda Calculi with Classical Control: Syntax and Expressive
  Power},
    author={Ugo Dal Lago, Andrea Masini, Margherita Zorzi},
    journal={arXiv preprint arXiv:cs/0703152},
    year={2007},
    archivePrefix={arXiv},
    eprint={cs/0703152},
    primaryClass={cs.LO}
}