\input zb-basic
\input zb-ioport
\iteman{io-port 06286004}
\itemau{Vizzotto, Juliana Kaizer; Calegaro, Bruno Crestani; Piveta, Eduardo Kessler}
\itemti{A double effect $\lambda $-calculus for quantum computation.}
\itemso{Du Bois, Andr\'e Rauber (ed.) et al., Programming languages. 17th Brazilian symposium, SBLP 2013, Bras{\'\i}lia, Brazil, October 3 -- 4, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40921-9/pbk). Lecture Notes in Computer Science 8129, 61-74 (2013).}
\itemab
Summary: In this paper we present a double effect version of the simply typed $\lambda $-calculus where we can represent both pure and impure quantum computations. The double effect calculus comprises a quantum arrow layer defined over a quantum monadic layer. In previous works we have developed the quantum arrow calculus, a calculus where we can consider just impure (or mixed) quantum computations. Technically, here we extend the quantum arrow calculus with a construct (and equations) that allows the communication of the monadic layer with the arrow layer of the calculus. That is, the quantum arrow is defined over a monadic instance enabling to consider pure and impure quantum computations in the same framework. As a practical contribution, the calculus allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. We also define equations for algebraic reasoning of computations involving measurements.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-40922-6\_5}
\end