nLab Benoît Valiron

• personal page

• github page

• InSpire page

• MathGenealogy page

Selected writings

Early consideration of quantum programming languages as quantum lambda-calculus invoking linear types:

• Benoît Valiron, A functional programming language for quantum computation with classical control, MSc thesis, University of Ottawa (2004) [doi:10.20381/ruor-18372, pdf]

• Peter Selinger, Benoît Valiron, A lambda calculus for quantum computation with classical control, Proc. of TLCA 2005 [arXiv:cs/0404056, doi:10.1007/11417170_26]

• Peter Selinger, Benoît Valiron, Quantum Lambda Calculus, in: Semantic Techniques in Quantum Computation, Cambridge University Press (2009) 135-172 [doi:10.1017/CBO9781139193313.005, pdf]

• Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron, A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus, EPTCS 88 (2012) 1-15 [arXiv:1012.4032, doi:10.4204/EPTCS.88.1]

[Selinger (2016):] When the QPL workshop series was first founded, it was called “Quantum Programming Languages”. One year I wasn’t participating, and while I wasn’t looking they changed the name to “Quantum Physics and Logic” — same acronym!

Back in those days in the early 21st century we were actually trying to do programming languages for quantum computing $[$Selinger & Valiron 2004$]$, but the sad thing is: In those days nobody really cared. $[...]$

Now it’s 15 years later and several of these parameters have changed: There has been a renewed interest, from government agencies and also from companies who are actually building quantum computers. $[...]$.

So now people are working on quantum programming languages again.

Implementation as an embedded programming language in Haskell:

• Richard Eisenberg, Benoît Valiron, Steve Zdancewic, Typechecking Linear Data: Quantum Computation in Haskell [pdf]

Introducing the functional quantum programming language Quipper:

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948:110-124, Springer, 2013 (arXiv:1304.5485)

• Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)

On linear algebra (finite-dimensional vector spaces over finite fields) as categorical semantics for linear logic/linear type theory:

• Benoît Valiron, Steve Zdancewic, Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi, in: Proc. of ICTAC’14, Lecture Notes in Computer Science 8687, Springer (2014) 442-459 [arXiv:1406.1310, doi:10.1007/978-3-319-10882-7_26, slides:pdf, pdf]

Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper-language:

• Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 [doi:10.1145/2699415, pdf, web, promo vid:YT]

On dynamic lifting (of quantum measurement-results) in quantum programming/quantum computing:

• Dongho Lee, Sebastien Bardin, Valentin Perrelle, Benoît Valiron, Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control, talk at Journées Informatique Quantique 2019 (Nov 2019) [pdf, pdf]

• Dongho Lee, Valentin Perrelle, Benoît Valiron, Zhaowei Xu, Concrete Categorical Model of a Quantum Circuit Description Language with Measurement, Leibniz International Proceedings in Informatics 213 (2021) 51:1-51:20 [arXiv:2110.02691, doi:10.4230/LIPIcs.FSTTCS.2021.51]

On software verification (formal methods) for quantum computing/quantum algorithms:

• Christophe Chareton, Sébastien Bardin, Dongho Lee, Benoît Valiron, Renaud Vilmart, Zhaowei Xu, Formal Methods for Quantum Programs: A Survey, in: Handbook of Formal Analysis and Verification in Cryptography, CRC (2023) [arXiv:2109.06493, doi:10.1201/9781003090052]

See also:

• Kostia Chardonnet, Marc de Visme, Benoît Valiron, Renaud Vilmart, The Many-Worlds Calculus [arXiv:2206.10234]

Related entries

• software verification

category: people