I am one of the developers of the
scalable programming
language, Quipper. Several
publications stem from that work: a paper at PLDI
2013, a paper at the workshop RC 2013, and
a featured article
in the August 2015 issue of CACM.
Ph.D Students
Present:
Thea Li. Started in Fall 2024. Co-supervision with Vladimir
Zamdzhiev. Topic of research: Categorical analysis of the
Heisenberg-Schrödinger duality.
Julien Lamiroy. Started in Winter 2024. Co-supervision with
Renaud Vilmart, in the context of the ANR TAQC.
Jérome Ricciardi. Started in Winter 2022. Co-supervision with
Christophe Chareton (CEA-LIST/LSL). Topic of research: Deductive
verification for quantum programs.
Nicolas Heurtel. Started in
Winter 2022. Co-supervision with Pablo Arrighi (LMF) and Shane
Mansfield (Quandela). Topic of the research: Formal methods for
Quantum Linear Optic.
Past:
Louis
Lemonnier, Ph.D student at LMF, UPSaclay,
2021-2024 🕮.
Co-supervision with Vladimir Zamdzhiev (Inria).
Abstract: While recent progress in quantum hardware open the
door for significant speedup in certain key areas, quantum algorithms
are still hard to implement right, and the validation of such quantum
programs is a challenge. Early attempts either suffer from the lack of
automation or parametrized reasoning, or require the user to write
specifications and algorithms far from those presented in research
articles or textbooks, and as a consequence, no significant quantum
algorithm implementation has been currently verified in a
scale-invariant manner. We propose QBRICKS, the first development
environment for certified quantum programs featuring clear separation
between code and proof, scale-invariance specification and proof, high
degree of proof automation and allowing to encode quantum programs in
a natural way, i.e. close to textbook style. This environment features
a new domain-specific language for quantum programs, namely
QBRICKS-DSL, together with a new logical specification language
QBRICKS-SPEC . Especially, we introduce and intensively build upon
HOPS, a higher-order extension of the recent path-sum semantics, used
for both specification (parametrized, versatile) and automation
(closure properties). QBRICKS builds on best practice of formal
verification for the classic case and tailor them to the quantum
case. To illustrate the opportunity of QBRICKS , we implement the
first scale-invariant verified implementations of non-trivial quantum
algorithms, namely phase estimation (QPE) -- the purely quantum part
of Shor algorithm for integer factoring -- and Grover search. It
proves by fact that applying formal verification to real quantum
programs is possible and should be further developed.
Quantum circuits synthesis using Householder transformations
With Timothée Goubault de Brugière, Marc Baboulin and Cyril
Allouche. Computer Physics
Communication248:107001
(2020).
Abstract: The synthesis of a quantum circuit consists in
decomposing a unitary matrix into a series of elementary
operations. In this paper, we propose a circuit synthesis method based
on the QR factorization via Householder transformations. We provide a
two-step algorithm: during the first step we exploit the specific
structure of a quantum operator to compute its QR factorization, then
the factorized matrix is used to produce a quantum circuit. We analyze
several costs (circuit size and computational time) and compare them
to existing techniques from the literature. For a final quantum
circuit twice as large as the one obtained by the best existing
method, we accelerate the computation by orders of magnitude..
Synthesizing Quantum Circuits via Numerical Optimization
With Timothée Goubault de Brugière, Marc Baboulin and Cyril
Allouche. 19th International Conference on Computational Science
(ICCS 2019), Faro, Portugal, June 12-14,
2019. LNCS
11537, pp. 3-16, 2019.
Abstract: We provide a simple framework for the synthesis of
quantum circuits based on a numerical optimization algorithm. This
algorithm is used in the context of the trapped-ions technology. We
derive theoretical lower bounds for the number of quantum gates
required to implement any quantum algorithm. Then we present numerical
experiments with random quantum operators where we compute the optimal
parameters of the circuits and we illustrate the correctness of the
theoretical lower bounds. We finally discuss the scalability of the
method with the number of qubits.
Realizability in the Unitary Sphere
With Alejandro Díaz-Caro, Mauricio Guillermo and Alexandre
Miquel. 34th Annual ACM/IEEE Symposium on Logic in Computer
Science(LICS 2019), Vancouver, BC, Canada, June 24-27,
2019. Pages
1-13, 2019.
Abstract:In this paper we present a semantics for a linear
algebraic lambda-calculus based on realizability. This semantics
characterizes a notion of unitarity in the system, answering a long
standing issue. We derive from the semantics a set of typing rules for
a simply-typed linear algebraic lambda-calculus, and show how it
extends both to classical and quantum lambda-calculi.
From Symmetric Pattern-Matching to Quantum Control
With Amr Sabry and Juliana Kaiser-Vizzotto. International
Conference on Foundations of Software Science and Computation
Structures (FoSSaCS'18), Apr 2018, Thessaloniki,
Greece. LNCS
10803, pp. 348-364.
Abstract: One perspective on quantum algorithms is that they
are classical algorithms having access to a special kind of memory
with exotic properties. This perspective suggests that, even in the
case of quantum algorithms, the control flow notions of sequencing,
conditionals, loops, and recursion are entirely classical. There is
however, another notion of control flow, that is itself quantum. The
notion of quantum conditional expression is reasonably
well-understood: the execution of the two expressions becomes itself a
superposition of executions. The quantum counterpart of loops and
recursion is however not believed to be meaningful in its most general
form. In this paper, we argue that, under the right circumstances, a
reasonable notion of quantum loops and recursion is possible. To this
aim, we first propose a classical, typed, reversible language with
lists and fixpoints. We then extend this language to the closed
quantum domain (without measurements) by allowing linear combinations
of terms and restricting fixpoints to structurally recursive fixpoints
whose termination proofs match the proofs of convergence of sequences
in infinite-dimensional Hilbert spaces. We additionally give an
operational semantics for the quantum language in the spirit of
algebraic lambda-calculi and illustrate its expressiveness by modeling
several common unitary operations.
Reuse method for quantum circuit synthesis
With Cyril Allouche, Marc Baboulin and Timothée Goubault de
Brugière (main author). International Conference: Applied
Mathematics, Modeling and Computational Science (AMMCS 2017), Aug
2017, Waterloo, Canada. Proceedings of AMMCS 2017, 2018.
Abstract: The algebraic decomposition of a unitary operator
is a key operation in the synthesis of quantum circuits. If most
methods factorize the matrix into products, there exists a method that
allows to reuse already existing optimized circuits to implement
linear combinations of them. This paper presents an attempt to extend
this method to a general framework of circuit synthesis. The method
needs to find suitable groups for the implementation of new quantum
circuits. We identify key points necessary for the construction of a
comprehensive method and we test potential group candidates.
A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing
With Hai Nguyen Van (main author), Thibaut Balabonski, Frédéric
Boulanger, Chantal Keller and Burkhart Wolff. In Proceedings of
FORMATS'17, LNCS
vol. 10419, pp. 318-334, 2017.
Abstract:
TESL addresses the specification of the temporal aspects of an
architectural composition language that allows the composition of
timed subsystems. TESL specifies the synchronization points between
events and time scales. Methodologically, subsystems having
potentially different models of execution are abstracted to their
interfaces expressed in terms of timed events.
In this paper, we present an operational semantics of TESL for
constructing symbolic traces that can be used in an online-test scenario:
the symbolic trace containing a set of constraints over time-stamps and
occurrences of events is matched against concrete runs of
the system.
We present the operational rules for building symbolic traces and
illustrate them with examples. Finally, we show a prototype implementation
that generates symbolic traces, and its use for testing
The Vectorial Lambda-Calculus
With Pablo Arrighi and Alejandro Díaz-Caro. Information and
Computation, 254(1):105-139,
2017.
Abstract: We describe a type system for the linear-algebraic
lambda-calculus. The type system accounts for the linear-algebraic
aspects of this extension of lambda-calculus: it is able to statically
describe the linear combinations of terms that will be obtained when
reducing the programs. This gives rise to an original type theory
where types, in the same way as terms, can be superposed into linear
combinations. We prove that the resulting typed lambda-calculus is
strongly normalizing and features a weak subject reduction. Finally,
we show how to naturally encode matrices and vectors in this typed
calculus.
Concrete Resource Analysis of the Quantum Linear System Algorithm used to Compute the Electromagnetic Scattering Cross Section of a 2D Target
With Artur Scherer, Siun-Chuon Mau, Scott Alexander, Eric van den
Berg and Thomas E. Chapuran. Quantum Information
Processing, 16:60,
2017.
This paper is an upgraded version of
a draft from 2015
previously named "Resource analysis of the quantum linear system
algorithm", written with the same co-authors.
Abstract: We provide a detailed estimate for the logical
resource requirements of the quantum linear system algorithm (QLSA)
[Phys. Rev. Lett. 103, 150502 (2009)] including the recently described
generalization [Phys. Rev. Lett. 110, 250504 (2013)]. Our resource
estimates are based on the standard quantum-circuit model of quantum
computation; they comprise circuit width, circuit depth, the number of
qubits and ancilla qubits employed, and the overall number of
elementary quantum gate operations as well as more specific gate
counts for each elementary fault-tolerant gate from the standard set
{X, Y, Z, H, S, T, CNOT}. To perform these estimates, we used an
approach that combines manual analysis with automated estimates
generated via the Quipper quantum programming language and
compiler. Our estimates pertain to the example problem size
N=332,020,680 beyond which, according to a crude big-O complexity
comparison, QLSA is expected to run faster than the best known
classical linear-system solving algorithm. For this problem size, a
desired calculation accuracy 0.01 requires an approximate circuit
width 340 and circuit depth of order 10^25 if oracle costs are
excluded, and a circuit width and depth of order 10^8 and 10^29,
respectively, if oracle costs are included, indicating that the
commonly ignored oracle resources are considerable. In addition to
providing detailed logical resource estimates, it is also the purpose
of this paper to demonstrate explicitly how these impressively large
numbers arise with an actual circuit implementation of a quantum
algorithm. While our estimates may prove to be conservative as more
efficient advanced quantum-computation techniques are developed, they
nevertheless provide a valid baseline for research targeting a
reduction of the resource requirements, implying that a reduction by
many orders of magnitude is necessary for the algorithm to become
practical.
The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects
With Ugo Dal Lago, Claudia Faggian and Akira Yoshimizu. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Paris, France, January 15 - 21, 2017,pp. 833--845.
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.
Generating reversible circuits from higher-order functional programs
In Proceedings of the 8th International Conference on Reversible Computation (RC'16), Bologna, Italy, July 7-8, 2016.LNCS vol. 9720, pp. 289-306.
Abstract: Boolean reversible circuits are boolean circuits made of reversible
elementary gates. Despite their constrained form, they can simulate
any boolean function. The synthesis and validation of a reversible
circuit simulating a given function is a difficult problem. In 1985,
Bennett proposed to generate reversible circuits from traces of
execution of Turing machines.
In this paper, we propose a novel presentation of this approach,
adapted to higher-order programs. Starting with a PCF-like language,
we use a monadic representation of the trace of execution to turn a
regular boolean program into a circuit-generating code. We show that a
circuit traced out of a program computes the same boolean function as
the original program.
Programming the Quantum Future
With Neil J. Ross, Peter Selinger, D. Scott Alexander and Jonathan M. Smith.
Communications of the ACM,
Vol. 58 No. 8, Pages 52-61, 2015.
This paper was the CACM featured article of August 2015, and a video
was made to advertise it. The producer was the very
kind Tom Geller. I met him for 3
hours in Waterloo (ON, Canada). Out of our very entertaining meeting
he made this excellent introduction to the topic of quantum
programming languages.
Towards a formal semantics of the TESL specification language
With Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Safouan Taha, Burkhart Wolff and Lina Ye. In GEMOC+MPM@MoDELS 2015, Ottawa, Canada, September 28, 2015, CEUR Workshop Proceedings, Vol. 1511, pp. 14--19.
Abstract: Most relevant industrial modeling problems depict
heterogeneity issues when combining different paradigms. Designing
such systems with discrete and continuous parts necessarily raises
formal verification problems. We focus on a synchronous
heterogeneous specification language, called TESL. In particular, it
allows the expression of interrelations of clocks and --- unlike
other existing languages --- is able to express
time-triggered behaviors above event-triggered ones. We are interested in formalizing
such a language to derive a verification framework, including model-checking, and testing.
The long-term purpose of this work is to develop in the Isabelle/HOL proof assistant, a formal semantics
for such a language. In the current paper, we present and compare three complementary semantic approaches for
our problem.
Parallelism and Synchronization in an Infinitary Context
With Ugo Dal Lago, Claudia Faggian and Akira Yoshimizu. Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Pages 559-572, 2015.
Abstract:
We study multitoken interaction machines in the context of a very
expressive logical system with exponentials, fixpoints and
synchronization. The advantage of such machines is to provide models
in the style of the Geometry of Interaction, i.e., an interactive
semantics which is close to low-level implementation. On the one hand,
we prove that despite the inherent complexity of the framework,
interaction is guaranteed to be deadlock free. On the other hand, the
resulting logical system is powerful enough to embed PCF and to
adequately model its behaviour, both when call-by-name and when
call-by-value evaluation are considered. This is not the case for
single-token stateless interactive machines.
A Scalable Quantum Programming Language
Plenary talk at the Institute for Quantum Computing (Waterloo, Canada), for the Workshop on Quantum Programming and Circuits in June 2015.
Summary:
The field of quantum algorithms is vibrant. However, these algorithms are usually described using mathematical formalism on paper and with hand-made descriptions of circuits. In order to move from the level of toy-size to practical scale, there is a need for quantum programming languages. Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and is able to generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.
The talk is available on youtube, see on the left.
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces
Scientific Annals of Computer
Science, 24(2):325-368,
2014.
The journal being open source, the paper can be
found there.
This paper builds on the conference paper entitled "Finite Vector
Spaces as Model of Simply-Typed Lambda-Calculi" which appeared in
Proceedings of the 11th International Colloquium on Theoretical
Aspects of Computing (ICTAC 2014)
,
LNCS vol. 8687, 2014, pp 442-459.
The revised paper is accessible on
[arXiv:1406.1310].
Abstract: In this paper we use finite vector spaces (finite
dimension, over finite fields) as a non-standard computational model
of linear logic. We first define a simple, finite PCF-like
lambda-calculus with booleans, and then we discuss two finite models,
one based on finite sets and the other on finite vector spaces. The
first model is shown to be fully complete with respect to the
operational semantics of the language, while the second model is
not. We then develop an algebraic extension of the finite lambda
calculus and study two operational semantics: a call-by-name and a
call-by-value. These operational semantics are matched with their
corresponding natural denotational semantics based on finite vector
spaces. The relationship between the various semantics is analyzed,
and several examples based on Church numerals are presented.
Applying quantitative semantics to higher-order quantum computing
Abstract:
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the language to an unusably small finitary fragment, or giving up important features of quantum physics such as entanglement. In this paper, we propose a denotational semantics for a quantum lambda calculus with recursion and an infinite data type, using constructions from quantitative semantics of linear logic.
An Introduction to Quantum Programming in Quipper
With A.S. Green, P.L. Lumsdaine, N.J. Ross and P. Selinger.
Proceedings of the 5th Conference on Reversible Computation (RC 2013),
Victoria, Canada, 2013.. LNCS 7948, 2013, pp. 110-124,
Abstract:
Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial introduction to the language, through a demonstration of how to make use of some of its key features. We illustrate many of Quipper’s language features by developing a few well known examples of Quantum computation, including quantum teleportation, the quantum Fourier transform, and a quantum circuit for addition.
Quipper: A Scalable Quantum Programming Language
With A. S. Green, P. L. Lumsdaine, N. J. Ross and P. Selinger. Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2013), ACM SIGPLAN Notices, Volume 48 Issue 6, June 2013, pp. 333-342.
Abstract:
The field of quantum algorithms is vibrant. Nevertheless, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and is able to generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.
Quantum Computation: a Tutorial
New Generation Computing, 30(4):271-296, September 2012. Ohmsha, Ltd and Springer.
Abstract:
This tutorial is the first part of a series of two articles on
quantum computation. In this first paper, we present the field of quantum
computation from a broad perspective. We review the mathematical
background and informally discuss physical implementations of quantum
computers. Finally, we present the main constructions specific to quantum
computation yielding algorithms.
Abstract:
This paper is the second part of a series of two articles on
quantum computation. If the first part was mostly concerned with the
mathematical formalism, here we turn to the programmer's perspective.
We analyze the various existing models of quantum computation and
the problem of the stability of quantum information. We discuss the
needs and challenges for the design of a scalable quantum programming
language. We then present two interesting approaches and examine their
strengths and weaknesses. Finally, we take a step back, and review the
state of the research on the semantics of quantum computation, and how
this can help in achieving some of the goals.
Abstract:
We show that quantum theory allows for transformations of black boxes that cannot be realized by inserting the input black boxes within a circuit in a pre-defined causal order. The simplest example of such a transformation is the classical switch of black boxes, where two input black boxes are arranged in two different orders conditionally on the value of a classical bit. The quantum version of this transformation---the quantum switch---produces an output circuit where the order of the connections is controlled by a quantum bit, which becomes entangled with the circuit structure. Simulating these transformations in a circuit with fixed causal structure requires either postselection, or an extra query to the input black boxes.
Typechecking Linear Data: Quantum Computation in Haskell
Draft, with R. Eisenberg and S. Zdancewic. June 2012.
Download: [pdf]. The Haskell code is accessible here (works with ghc 7.4.1).
Abstract:
This paper demonstrates how to use type classes to get Haskell's
type inference engine to infer the types of an embedded language for
quantum computation. The embedded language, a variant of Selinger
and Valiron's quantum lambda calculus (QLC), uses linear
types to express the non-duplicability of quantum data, along with
subtyping to allow convenient mixing of classical data with quantum
data. The embedding makes sophisticated use of Haskell's type
classes to do logic programming at the type level.
A Type System for the Vectorial Aspects of the Linear-Algebraic Lambda-Calculus
With P. Arrighi and A. Díaz-Caro. In Elham Kashefi, Jean Krivine and Femke van Raamsdonk: Proceedings of the 7th workshop on Developments in
Computational Models (DCM 2011). EPTCS 88, pp. 1–15.
Published: 30th July 2012.
Download: [arXiv:1012.4032] (31 pages with appendix, preprint). The coq proof advertised in the paper is here.
This is an updated version of a draft entitled Subject reduction in a Curry-style polymorphic type system with a vectorial structure, dated from December 2010.
Abstract:
In this paper we describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors. The type system is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.
Equivalence of Algebraic Lambda-Calculi (Extended Abstract)
With A. Díaz-Caro, S. Perdrix and C. Tasson. Proceedings of the
5th International Workshop on Higher-Order Rewriting (HOR'10), Edinburgh, July 14 2010.
An extended version with proofs can be found on arXiv:1005.2897. The coq proof advertised in the paper is here.
Abstract: We examine the relationship between the algebraic
lambda-calculus (λ-alg) (Vaux 2009), a fragment of the
differential lambda calculus of Ehrhard and Regnier (2003), and the
linear-algebraic lambda-calculus (λ-lin) of Arrighi and Dowek
(2008), a lambda calculus for quantum computing. Both calculi are
algebraic in the sense that linear combinations of lambda-terms are
allowed. While it is known that λ-lin can simulate λ-alg, we
answer the question of the reverse simulation of λ-lin by
λ-alg Our proof relies on the observation that λ-lin is
essentially call-by-value, while λ-alg is call-by-name, leading
to a simulation based on an algebraic extension of the continuation
passing style. This result is a step towards an algebraic extension of
call-by-value / call-by-name duality in the lambda-calculus.
A Typed, Algebraic, Computational Lambda-Calculus
Mathematical Structures in Computer Science, 23(2):504-554, 2013.
This paper builds on the extended abstract entitled "Semantics of a Typed Algebraic Lambda-Calculus" which appeared in S. B. Cooper, P. Panangaden and E. Kashefi, Proceedings of the 6th workshop on Developments in Computational Models, Edinburgh, 9 – 10 July 2010. Volume 26 of Electronic Proceedings in Theoretical Computer Science, pages 147-158. [pdf] (12 pages, revised version).
An earlier version of this work entitled About Typed Algebraic Lambda-Calculi and dated from January 2009 has also been accessible on this website as a draft.
Abstract:
Lambda-calculi with vectorial structures have been studied in
various ways, but their semantics remain mostly untouched. The main
contribution of this paper is to provide a categorical framework for
the semantics of such algebraic lambda-calculi.
We first develop a categorical analysis of a general simply-typed
lambda-calculus endowed with a structure of module. We study the
problems arising from the addition of a fixed point combinator and
show how to modify the equational theory to solve them. The
categorical analysis carries nicely over to the modified language.
We provide various concrete models,
both for the case without fixpoints and the case with fixpoints.
Abstract:
Directly encoding lambda-terms on quantum strings while keeping a
quantum interpretation is a hard task. As shown by
van Tonder (2004), requiring a unitary reduction forces the
lambda-terms in superposition to be mostly equivalent.
Following instead Arrighi and Díaz-Caro (2009), we show in this note how one can
conceive a lambda-calculus with algebraic features and that
admits a general notion of orthogonality amongst lambda-terms, by
providing a compiler of the system into unitary maps.
Chapter, with Peter Selinger. In S. Gay and I. Mackie (Editors), Semantic Techniques in Quantum Computation, Cambridge University Press, pp. 135-172, 2009.
Abstract:
The objective of this thesis is to develop a semantics for higher order quantum information.
Following the work done in the author's M.Sc. thesis, we study a lambda calculus for quantum
computation with classical control. The language features two important properties. The first one,
arising from the so-called no-cloning theorem of quantum computation, is the need for a distinction
between duplicable and non-duplicable elements. For keeping track of duplicability at higher order,
we use a type system inspired by the resource-sensitive linear logic. The second important aspect is
the probability inherent to measurement, the only operation for retrieving classical data from quan-
tum data. This forces us into choosing a reduction strategy for being able to define an operational
semantics.
We address the question of a denotational semantics in two respects. First, we restrict the
study to the strictly linear aspect of the language. Doing so, we suppress the need for distinguishing
between duplicable and non-duplicable elements and we can focus on the description of quantum
features at higher order. Using the category of completely positive maps as a framework, we build
a fully abstract denotational model of the strictly linear fragment of the language.
The study of the full language is more demanding. For dealing with the probabilistic aspect of
the language, we use a method inspired by Moggi and build a computational model with a distinction
between values and computations. For the distinction between duplicability and non-duplicability in
the calculus, we adapt Bierman's linear category, where the duplication is considered as a comonad
with specific properties. The resulting model is what we call a linear category for duplication.
Finally, we only focus on the fragment of the language that contains the aforementioned elements,
and remove the classical Boolean and quantum Boolean features to get a generic computational
linear lambda-calculus. In this idealized setting, we show that such a language have a full and
complete interpretation in a linear category for duplication.
On Quantum and probabilistic linear lambda-calculi
Extended abstract. Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008),
Reykjavik, Iceland,
12-13 July 2008.ENTCS Volume 270, Issue 1, pp 121-128, 2011.
Abstract: In this paper we discuss a semantics for a linear higher-order probabilistic lambda-calculus in the light of the semantics of completely positive maps for quantum computation. We analyse the set of representable elements in this category and describe some of its properties. We then show how one can use this to derive information on the capabilities of higher-order quantum computation compared to probabilistic computation. Finally, we derive a sound and complete semantics for a subset of the probabilistic language.
The talk was filmed, see on the left.
A linear-non-linear model for a computational call-by-value lambda calculus
Extended abstract, with Peter Selinger. Proceedings of the 11th
International Conference on Foundation of Software Science and Computation
Structures (FOSSACS'08), Budapest, March 29 - April 6, 2008.Springer LNCS 4962, pp. 81-96, 2008.
Abstract: We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator "!" as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The "!" operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggi's computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.
On a fully abstract model for a quantum linear functional language
Extended abstract, with Peter Selinger. Proceedings of the 4th International Workshop on Quantum Programming Languages (QPL 2006), Oxford,
July 17-19, 2006. ENTCS Volume 210, pp. 123-137, 2008.
Abstract: This paper studies the linear fragment of the
programing language for quantum computation with classical control
described in [Selinger and Valiron, 2005]. We sketch the language, and
discuss equivalence of terms. We also describe a fully abstract
denotational semantics based on completely positive maps.
A lambda calculus for quantum computation with classical control
With Peter Selinger.
Mathematical Structures in Computer Science, 16(3):527-552, 2006.
An earlier version of this work entitled "Quantum typing" has appeared
in Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku,
Finland (QPL 2004), editor Peter Selinger, TUCS General Publication No 33,
Turku Centre for Computer Science, 2004.
Abstract: The objective of this paper is to develop a functional
programming language for quantum computers. We develop a lambda
calculus for the classical control model, following the first author's
work on quantum flow-charts. We define a call-by-value operational
semantics, and we give a type system using affine intuitionistic
linear logic. The main results of this paper are the safety properties
of the language and the development of a type inference algorithm.
A functional programming language for quantum
computation with classical control
Abstract:
The objective of this thesis is to develop a functional programming
language for quantum computers based on the QRAM model,
following the work of P. Selinger (2004) on quantum flow-charts. We
construct a lambda-calculus without side-effects to deal with quantum
bits. We equip this calculus with a probabilistic call-by-value
operational semantics. Since quantum information cannot be duplicated
due to the no-cloning property, we need a resource-sensitive
type system. We develop it based on affine intuitionistic linear
logic. Unlike the quantum lambda-calculus proposed by Van Tonder
(2003, 2004), the resulting lambda-calculus has only one
lambda-abstraction, linear and non-linear abstractions being encoded
in the type system. We also integrate classical and quantum data types
within our language. The main results of this work are the
subject-reduction of the language and the construction of a type
inference algorithm.
![[picture of me]](images/moi7.jpg)