]> 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. Following this position, between 2009 and 2011 I was "ATER" (teaching and research post-doctoral position) successively in the Laboratoire d'Informatique de Grenoble (LIG) within the CAPP team, then at Université de Paris 13, in the team LCR of the Laboratoire d'Informatique de Paris Nord (LIPN). I am now post-doc at the Department of Computer and Information Science of the University of Pennsylvania.

Research interests

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

Papers

Typechecking Embedded Languages with Linearity Constraints in Haskell

Draft, with S. Zdancewic. June 2011.

Download: [pdf]. The Haskell code is accessible here (works with ghc 7.0.3).

Abstract: We aim at implementing the quantum lambda-calculus of Selinger-Valiron as an embedded language in Haskell. The main difficulty is to deal with the linearity constraints of the type system, which take the form of a special flag "!" that can be set on any type to indicate that one can duplicate an object of that type. The type system is equipped with a subtyping relation: one is never forced to duplicate a duplicable element. We show how the Haskell type checker can be programmed to do the type inference for us, using the logic programming feature of type classes. We describe the source language, how it is embedded in Haskell, and we discuss a few examples.

A Type System for the Vectorial Aspects of the Linear-Algebraic Lambda-Calculus

With P. Arrighi and A. Díaz-Caro. To appear in Proceedings of the 7th workshop on Developments in Computational Models (DCM 2011).

Download: [arXiv:1012.4032] (31 pages, 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. Pre-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

Accepted for publication in Mathematical Structures in Computer Science.

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.

Orthogonality and Algebraic Lambda-Calculus (Extended Abstract)

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

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

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.