I defended my *Habilitation à Diriger des Recherches* on
Sept 24, 2024. See the corresponding webpage for
details.

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.

- 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).
- Kostia Chardonnet. Ph.D student at LMF, UPSaclay, 2019-2023 🕮. Co-supervision with Alexis Saurin (IRIF).
- Agustin Borgna. Ph.D student at LMF, UPSaclay and LORIA, ULorraine, 2019-2023 🕮. Co-supervision with Simon Perdrix (LORIA).
- 이동호 (Dong-Ho Lee). Ph.D student at CEA-LIST and LRI, UPSaclay, 2018-2022 🕮. Co-supervision with Valentin Perrelle at CEA-LIST.
- Timothée Goubault de Brugière. Ph.D student at LRI, UPSaclay, 2017-2020 🕮. Co-supervision with Marc Baboulin.
- Yann Hamdaoui, Ph.D. student at IRIF, Paris 7, 2014-2018 🕮. Co-supervision with Claudia Faggian.

- Present
- None

- Past
- Srijita Nandi. Student from
*Université Paris Saclay*, Master Intership (M1 QDCS). 2024. - Julien Lamiroy. Student from
*ENS Paris Saclay*, Master internship (M2). 2023. - Nicolas Heurtel. Student from
*CentraleSupélec (formerly "École Centrale Paris")*in a special research program. - Kostia Chardonnet, Master internship (stage M2 MPRI). Co-supervised with Alexis Saurin.
- Nicolas Nalpon, Master internship (stage M2 MPRI). 2018
- Skander Kazdaghli, student from CentraleSupelec. Summer internship co-supervised with Marc Baboulin at LRI. 2018.
- Alexandre Clément, Master internship (stage M2 LMFI). Co-supervised with Michele Pagani at IRIF (Paris 7). 2018.
- Baptiste Colin, final internship of engineering school Mines-ParisTech. 2018.
- Nicolas Blanco, Master student (stage M2 LMFI). 2015.

- Srijita Nandi. Student from

Here is a list of my published and unpublished papers. All of my old papers are there, but I've lost track at some point. For more recent papers, see

- HAL (there is an institutional obligation to store them here)
- dblp (much cleaner, but misses non-CS papers)

Download: [arXiv:2003.05841].

**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.

**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..

**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.

Download: [arXiv:1904.08785] (extended version).

**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.

Download: [arXiv:1804.00952] (long version).

**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.

Download: [hal-01711378] (draft).

**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.

Download: [hal-01583815] (draft).

**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

Download: [arXiv:1308.1138] (draft).

**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.

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.

Download: [arXiv|Open Access]

**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.

**Download:** [arXiv extended version]

**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.

**Download:** [arXiv extended version]

**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.

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.

**Download:** [on ceur-ws.org]

**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.

Download: [pdf] (long version)

**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.

**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.

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.

Download: [arXiv:1311.2290] (revised paper)

**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.

Download: [arXiv:1304.5485] (preprint).

**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.

Download: [arXiv:1304.3390] (preprint).

The language *Quipper* is available online at the address http://www.mathstat.dal.ca/~selinger/quipper/.

**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.

Download: [draft]

**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.

Copyright © Ohmsha, Ltd and Springer.

Download: [draft]

**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.

Copyright © Ohmsha, Ltd and Springer.

Download: [arXiv:0912.0195].

**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.

©2013 American Physical Society

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.

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.

Download: [pdf] (6 pages, revised version).

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.

Download : [pdf] (revised version, 45 pages, 2011).

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.

Copyright © Cambridge University Press 2013.

Download: [pdf]

**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.

The presentation was filmed: see on the left.

Download: [pdf]

Download: [pdf] (Preprint)

Download: [pdf.gz] (219 pages, revised version)

Archived on TEL as oai:tel.archives-ouvertes.fr:tel-00483944_v1.

**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.

Download: [pdf.gz] (9 pages, preprint)

**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.

Download: [pdf] (15 pages, preprint)

Also available as arXiv:0801.0813.

**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.

Download: [dvi, ps, ps2up, pdf] (13 pages, preprint)

**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.

Download: [dvi, ps, ps2up, pdf] (26 pages)

A conference version is to be found in *Proceedings of the Seventh
International Conference on Typed Lambda Calculi and Applications
(TLCA 2005), Nara, Japan.* Springer
LNCS 3461, pp. 354-368, 2005. © 2005 Published by Springer.
Can be downloaded on arXiv.org:
cs.LO/0404056 (preprint).
The slides of the presentation are
here.

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.

Download: [pdf.gz] (130 pages, revised version)

**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.