We build on the series of work by Dal Lago and coauthors and identify proof nets (of linear logic) as higher-order quantum circuits. By accommodating quantum measurement using additive slices, we obtain a comprehensive framework for programming and interpreting quantum computation. Specifically, we introduce a quantum lambda calculus MLLqm and define its geometry of interaction (GoI) semantics - in the style of token machines - via the translation of terms into proof nets. Its soundness, i.e. invariance under reduction of proof nets, is established. The calculus MLLqm attains a pleasant balance between expressivity (it is higher-order and accommodates all quantum operations) and concreteness of models (given as token machines, i.e. in the form of automata). © 2014 Springer-Verlag.
CITATION STYLE
Yoshimizu, A., Hasuo, I., Faggian, C., & Dal Lago, U. (2014). Measurements in proof nets as higher-order quantum circuits. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 371–391). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_20
Mendeley helps you to discover research relevant for your work.