]> Benoît Valiron: Research

Presentation

[picture of me]

I did my first years of university in France, in Grenoble. Then I did a master and a Ph.D. in Mathematics under the supervision of Peter Selinger at the University of Ottawa. The Ph.D. defense took place on Thursday, September 25 2008. In 2008-2009, I was in a post-doc position funded by INRIA at the "Laboratoire d'Informatique de Polytechnique" within the research group TYPICAL. I am now in an "ATER" (teaching and research post-doctoral position) in the "Laboratoire d'Informatique de Grenoble" (LIG) within the CAPP team.

Research interests

You can find the list of my publications below.

Publications

Equivalence of Algebraic Lambda-Calculi (Extended Abstract)

With A. Díaz-Caro, S. Perdrix and C. Tasson. Accepted for publications in the proceedings of the 5th International Workshop on Higher-Order Rewriting (HOR'10), Edinburgh, July 14 2010.

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

An version with proofs can be found on arXiv:1005.2897.

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.

Semantics of a Typed Algebraic Lambda-Calculus

To appear in the proceedings of the 6th workshop on Developments in Computational Models, Edinburgh, 9 – 10 July 2010.

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

A previous version of this work was a draft dated from January 2009, entitled About Typed Algebraic Lambda-Calculi.

Abstract: Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We sketch the relation with two established vectorial lambda-calculi. Then we study the problems arising from the addition of a fixed point combinator and how to modify the equational theory to solve them. We sketch an algebraic vectorial PCF and its possible denotational interpretations.

Orthogonality and Algebraic Lambda-Calculus (Extended Abstract)

Accepted for presentation at QPL'10, Oxford, May 29-30 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.

Sums and Triangular Stacks of Integers

Draft. January 2010.

Download: [pdf]

Beyond Quantum Computers

Draft, with G. Chiribella, G. M. D'Ariano, P.Perinotti. November 2009.

Download: [arXiv:0912.0195]

Quantum Lambda Calculus

Chapter, with Peter Selinger. To appear in Semantic Techniques in Quantum Computation, published by Cambridge University Press.

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

On Quantum and probabilistic linear lambda-calculi

Extended abstract. To appear in Proceedings of the joint 5th QPL and 4th DCM: Quantum Physics and Logic and Development of Computational Models (QPL/DCM 2008), Reykjavik, 2008.

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.

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

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.