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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45: QuantumPOPL at Amphitheater 44
Chair(s): Michele PaganiIRIF, Université Paris Diderot
16:30 - 16:55
Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA
16:55 - 17:20
Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo
17:20 - 17:45
Jennifer Paykin, Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania