Measurements in Proof Nets as Higher-Order Quantum Circuits

Abstract : 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 frame-work for programming and interpreting quantum computation. Specifically, we introduce a quantum lambda calculus MLLqm and define its geometry of interac-tion (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 es-tablished. 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).
Document type :
Conference papers
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01091582
Contributor : Ugo Dal Lago <>
Submitted on : Friday, December 5, 2014 - 4:31:00 PM
Last modification on : Friday, January 4, 2019 - 5:32:59 PM
Long-term archiving on : Monday, March 9, 2015 - 6:04:44 AM

File

esop14extended.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian, Ugo Dal Lago. Measurements in Proof Nets as Higher-Order Quantum Circuits. 23rd European Symposium on Programming, Apr 2014, Grenoble, France. pp.371 - 391, ⟨10.1007/978-3-642-54833-8_20⟩. ⟨hal-01091582⟩

Share

Metrics

Record views

544

Files downloads

190