POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 16:55 - 17:20 at Amphitheater 44 - Quantum Chair(s): Michele Pagani

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove 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 model is obtained as an instance of a new framework:

  • we equip Geometry of Interaction with the ability to capture \emph{choice effects} in a parametric flexible way, via a memory structure;
  • we develop a general notion of parallel abstract rewrite system, which allows us to deal with the combination of parallelism and probabilistic choice in an infinitary setting;
  • our construction produces a multi-token machine, a proof-net system and a PCF-style language, where the multi-token machine is an adequate model of nets reduction, and the nets an adequate model of PCF-style terms rewriting.

Being based on a multi-token machine associated to a memory, our model has a concrete nature which makes it well suited to build low-level operational descriptions of higher-order languages.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45
QuantumPOPL at Amphitheater 44
Chair(s): Michele Pagani IRIF, Université Paris Diderot
Invariants of Quantum Programs: Characterisations and Generation
Mingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Ugo Dal Lago University of Bologna, France, Claudia Faggian , Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo
QWIRE: A Core Language for Quantum Circuits
Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania