Taming Non-compositionality Using New Binders

We propose an extension of the traditional λ-calculus in which terms are used to control an outside computing device (quantum computer, DNA computer...). We introduce two new binders: ν and ρ. In denotes an abstract resource of the outside computing device, whereas in ρx.M, x denotes a concrete resource. These two binders have different properties (in terms of α-conversion, scope extrusion, convertibility) than the ones of standard λ-binder. We illustrate the potential benefits of our approach with a study of a quantum computing language in which these new binders prove meaningful. We introduce a typing system for this quantum computing framework in which linearity is only required for concrete quantum bits offering a greater expressiveness than previous propositions.

• Type: Conference
• Year: 2007
• Where: UC
• Authors: Frédéric Prost
• Keywords: Computing Device, Quantum, Quantum Computer, UC 2007