[picture of me]


I am on the organising committee of the non-local events QPL'20 and MFPS'20. Please consider registering!

Project: Quipper

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

  • 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.
  • Louis Lemonnier. Started in Fall 2021. Co-supervision with Pablo Arrighi (LMF). Topic of the research: categorical semantics of quantum control.

Master Students

  • None
  • 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.

Internship proposals

You can find the list of my published and unpublished papers below.

Papers and Filmed presentations

Toward certified quantum programming

With Christophe Chareton, Sébastien Bardin, François Bobot and Valentin Perrelle. Draft, 2020.

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.

Quantum circuits synthesis using Householder transformations

With Timothée Goubault de Brugière, Marc Baboulin and Cyril Allouche. Computer Physics Communication 248: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.

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.

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.

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.

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.

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.

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.

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

The Vectorial Lambda-Calculus

With Pablo Arrighi and Alejandro Díaz-Caro. Information and Computation, 254(1):105-139, 2017.

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.

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.

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.

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.

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.

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.

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.

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.

Download: [on]

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.

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.

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

With Michele Pagani and Peter Selinger. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014). ACM SIGPLAN Notices, Volume 49, Issue 1, January 2014, pp. 647-658.

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.

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,

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.

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.

Download: [arXiv:1304.3390] (preprint).

The language Quipper is available online at the address

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.

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.

Quantum Computation: from a Programmer's Perspective

New Generation Computing, 31(1):1-26, January 2013. 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.

Quantum computations without definite causal structure

With G. Chiribella, G. M. D'Ariano and P. Perinotti. Physical Review A, 88:022318(2013), American Physical Society.

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

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.

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.

A Typed, Algebraic, Computational Lambda-Calculus

Mathematical Structures in Computer Science, 23(2):504-554, 2013.

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.

Orthogonality and Algebraic Lambda-Calculus (Extended Abstract)

In the proceedings of the 7th QPL workshop, Oxford, 29 – 30 mai 2010..

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.

Sums and Triangular Stacks of Integers

Draft. January 2010.

Download: [pdf]

Quantum Lambda Calculus

Chapter, with Peter Selinger. In S. Gay and I. Mackie (Editors), Semantic Techniques in Quantum Computation, Cambridge University Press, pp. 135-172, 2009.

Download: [pdf] (Preprint)

Semantics for a Higher Order Functional Programming Language for Quantum Computation.

Ph.D. Thesis, University of Ottawa, 2008.

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

Archived on TEL as

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.

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.

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.

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.

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.

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.

A lambda calculus for quantum computation with classical control

With Peter Selinger. Mathematical Structures in Computer Science, 16(3):527-552, 2006.

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

A functional programming language for quantum computation with classical control

M.Sc. Thesis, University of Ottawa, 2004.

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.