Measurements in Proof Nets as Higher-Order Quantum Circuits - Archive ouverte HAL Access content directly
Conference Papers Year : 2014

Measurements in Proof Nets as Higher-Order Quantum Circuits


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).
Fichier principal
Vignette du fichier
esop14extended.pdf (1.08 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01091582 , version 1 (05-12-2014)



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⟩
397 View
131 Download



Gmail Facebook Twitter LinkedIn More