The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

Abstract

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. The approach we develop is not specific to quantum computation, and our model is an instance of a new framework whose main feature is the ability to model commutative effects in a parallel setting. Being based on a multi-token machine equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages.

21 pages, extended version of the conference paper ; July 2017: removed a spurious and unused lemma

References in corpus (2)

• Quantum algorithm for solving linear systems of equations
• Wave-Style Token Machines and Quantum Lambda Calculi

Cited by in corpus (9)

• Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
• Confluence in Probabilistic Rewriting
• Quantum Temporal Logic
• Formal Methods for Quantum Programs: A Survey
• Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms
• The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter
• Transparent Synchronous Dataflow
• On Higher-Order Probabilistic Subrecursion
• The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version)