16STIC04 project
Foundations of Quantum Computation:
Syntax and Semantics

(Full project description)

Members of the project:
External collaborators:
Local organizer: Alejandro Díaz-Caro

Funded by

Organized by

First FoQCoSS Meeting
Universidad Nacional de Quilmes
Buenos Aires, December 5-16, 2016

Abstract of the project:
The design of quantum programming languages involves the study of many characteristics of languages which can be seen as special cases of classical systems: parallelism, probabilistic systems, non-deterministic systems, type isomorphisms, etc. This project proposes to study some of these characteristics, which are involved in quantum programming languages, but also have a more immediate utility in the study of nowadays systems.
In addition, from a more foundational point of view, we are interested in the implications of computer science principles for quantum physics. For example, the consequences of the Church-Turing thesis for Bell-like experiments: if some of the parties in a Bell-like experiment use a computer to decide which measurements to make, then the computational resources of an eavesdropper have to be limited in order to have a proper observation of non-locality. The final aim is to open a new direction in the search for a framework unifying computer science and quantum physics.

Kickoff workshop


Monday 5 Dec - Room 22
10.30 ► Gilles Dowek: Quantitative informational aspects in discrete physics
11.15 ► Pablo Arrighi: Discrete Lorentz covariance for quantum walks and quantum cellular automata
12.00 - Lunch
14.00 ► Christian de Ronde: On the physical foundation of quantum superpositions (beyond measurement outcomes and mathematical structures)
14.45 ► Simon Martiel: Quantum causal graph dynamics
15.30 - Coffee break
16.00 ► Stefano Facchini: Quantum walking in curved spacetime: (3+1) dimensions, and beyond
16.45 ► Juliana Kaizer Vizzotto (video-conferenced): A double effect lambda-calculus for quantum computation

Tuesday 6 Dec - Room 22
10.30 ► Benoît Valiron: A Geometry of interaction for quantum computation
11.15 ► Alejandro Díaz-Caro: Typing quantum superpositions and projective measurements
12.00 - Lunch
14.00 ► Gabriel Senno: Robust Bell inequalities from communication complexity
14.45 ► Ariel Bendersky: Non-signaling deterministic models for non-local correlations have to be uncomputable
15.30 - Coffee break
16.00 ► Renaud Vilmart: Completeness and Incompleteness of the ZX-Calculus, a diagrammatic language for quantum reasoning and computing
16.45 ► José Carlos Puiati (video-conferenced): Implementation of an interpreter and typechecker for the double effect quantum lambda calculus

For organizational reasons, if you plan to attend, please, send your name and affiliation to alejandro@diaz-caro.info

For the remaining days we will work in groups on the tasks of the project

Team 1: Consecuences of QC in Quantum Physics

Gabriel / Gilles / Pablo / Simon M / Stefano

Team 2: Lambda Calculus and QC

Alejandro / Benoît / José Carlos / Octavio / Renaud

Gilles Dowek - Quantitative informational aspects in discrete physics
Joint work with Pablo Arrighi
Discrete physics investigates the hypothesis that natural phenomena can be described using finite mathematics only. This hypothesis has a deep connection with another: that the density of information in nature is bounded. In this talk, I will discuss whether it is possible to measure the complexity of physical phenomena by the amount of information their description requires, focusing on three examples: free fall according to Newtonian physics, to Special Relativity and to General Relativity.

Pablo Arrighi - Discrete Lorentz covariance for quantum walks and quantum cellular automata
Joint work with Stefano Facchini and Marcelo Forets
We formalize a notion of discrete Lorentz transforms for Quantum Walks (QW) and Quantum Cellular Automata (QCA), in (1 + 1)-dimensional discrete spacetime. The theory admits a diagrammatic representation in terms of a few local, circuit equivalence rules. Within this framework, we show the first-order-only covariance of the Dirac QW. We then introduce the Clock QW and the Clock QCA, and prove that they are exactly discrete Lorentz covariant. The theory also allows for non-homogeneous Lorentz transforms, between non-inertial frames.

Christian De Ronde - On the physical foundation of quantum superpositions (beyond measurement outcomes and mathematical structures)
Quantum superpositions are being used today in laboratories all around the world in order to create the most outstanding technological and experimental developments of the last centuries. However, while many experimentalists are showing that Schroedinger's cats are growing fat, while it becomes more and more clear that quantum superpositions are telling us something about quantum physical reality even at the macroscopic scale, philosophers of QM in charge of analyzing and interpreting these mathematical expressions (through the many interpretations of QM that can be found in the literature) have not been capable of providing a coherent physical representation of them. In this paper we attempt to discuss the importance of providing a physical representation of quantum superpositions that goes beyond the mere reference to mathematical structures and measurement outcomes.

Simon Martiel - Quantum causal graph dynamics
Joint work with Pablo Arrighi
Consider a graph having quantum systems lying at each node. Suppose that the whole thing evolves in discrete time steps, according to a global, unitary causal operator. By causal we mean that information can only propagate at a bounded speed, with respect to the distance given by the graph. Suppose, moreover, that the graph itself is subject to the evolution, and may be driven to be in a quantum superposition of graphs---in accordance to the superposition principle. We show that these unitary causal operators must decompose as a finite-depth circuit of local unitary gates. This unifies a result on Quantum Cellular Automata with another on Reversible Causal Graph Dynamics. Along the way we formalize a notion of causality which is valid in the context of quantum superpositions of time-varying graphs, and has a number of good properties. Keywords: Quantum Lattice Gas Automata, Block-representation, Curtis-Hedlund-Lyndon, No-signalling, Localizability, Quantum Gravity, Quantum Graphity, Causal Dynamical Triangulations, Spin Networks, Dynamical networks, Graph Rewriting.

Stefano Facchini - Quantum walking in curved spacetime: (3+1) dimensions, and beyond
Joint work with Pablo Arrighi
A discrete-time Quantum Walk (QW) is essentially an operator driving the evolution of a single particle on the lattice, through local unitaries. Some QWs admit a continuum limit, leading to familiar PDEs (e.g. the Dirac equation). Recently it was discovered that prior grouping and encoding allows for more general continuum limit equations (e.g. the Dirac equation in (1+1) curved spacetime). In this paper, we extend these results to arbitrary space dimension and internal degree of freedom. We recover an entire class of PDEs encompassing the massive Dirac equation in (3+1) curved spacetime. This means that the metric field can be represented by a field of local unitaries over a lattice.

Juliana Kaizer Vizzotto - (Videoconference) A double effect lambda-calculus for quantum computation
In this talk we present a double effect version of the simply typed lambda-calculus in which we can represent both pure and impure quantum computations. The double effect calculus comprises a quantum arrow layer defined over a quantum monadic layer. Technically, we propose a new construct in the calculus (and equations) that allows the communication of the monadic layer with the arrow layer of the calculus. That is, the quantum arrow is defined over a monadic instance, enabling to consider both pure and impure quantum computations in the same framework. As a practical contribution, the calculus allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. We also define equations for algebraic reasoning of computations involving measurements.

Benoît Valiron - A geometry of interaction for quantum computation
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. It is parametric on an algebraic notion of memory. This way, it can model quantum, but also classical and purely probabilistic computations. 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.

Alejandro Díaz-Caro - Typing quantum superpositions and projective measurements
Joint work with Gilles Dowek
We study a purely functional quantum extension of lambda calculus, that is, an extension of lambda calculus to express some quantum features, where the quantum memory is abstracted out. This calculus is a typed extension of the first-order linear-algebraic lambda-calculus. The type is linear on superpositions, so to forbid from cloning them, while allows to clone basis vectors.

Gabriel Senno - Robust Bell inequalities from communication complexity
Joint work with Sophie Laplante, Mathieu Laurière, Alexandre Nolin and Jérémie Roland
We contribute to the study of the relationship between nonlocality and the advantage that quantum mechanics offers in communication complexity by showing how to obtain large Bell violations for quantum distributions, from any gap between quantum communication complexity and the classical partition bound. This applies to most of the usually studied functions (Disjointness, Vector in Subspace, Tribes, etc). The violations obtainable from our construction are resistant to the detection loophole and, at the expense of an increase in the number of outputs, can be also made resistant to uniform noise.

Ariel Bendersky - Non-signaling deterministic models for non-local correlations have to be uncomputable
Joint work with Gabriel Senno, Gonzalo de la Torre, Santiago Figueira and Antonio Acin
Quantum mechanics postulates random outcomes. However, a model making the same output predictions but in a deterministic manner would be, in principle, experimentally indistinguishable from quantum theory. In this work we consider such models in the context of non-locality on a device independent scenario. That is, we study pairs of non-local boxes that produce their outputs deterministically. It is known that, for these boxes to be non-local, at least one of the boxes' output has to depend on the other party's input via some kind of hidden signaling. We prove that, if the deterministic mechanism is also algorithmic, there is a protocol which, with the sole knowledge of any upper bound on the time complexity of such algorithm, extracts that hidden signaling and uses it for the communication of information.

Renaud Vilmart - Completeness and Incompleteness of the ZX-Calculus, a diagrammatic language for quantum reasoning and computing
Joint work with Emmanuel Jeandel, Simon Perdrix and Quanlong Wang
The ZX-Calculus introduced by Bob Coecke and Ross Duncan is a diagrammatic language for quantum reasoning, and can in fact be seen as a generalisation of quantum circuitry. It is universal, and comes with a set of transformation rules that preserve the represented matrix. The stabiliser and real stabiliser quantum mechanics can be represented in the language, and they have been proven to be complete. The Clifford+T group is also expressible in the language, but its completeness in general is an open question, though it has been proven for a single qubit. Recently, a rule called supplementarity has been introduced and it has been proven it could not be derived from the others in the Clifford+T group. We can show that the restriction of the language to the Clifford+T is still not complete by introducing yet another rule. This one in addition with the supplementarity makes two other rules derivable. Moreover, we can shown that the supplementarity can be generalised to any natural number, and that it is not derivable in an infinite number of fragments.

José Carlos Puiati - (Videoconference) Implementation of an interpreter and typechecker for the double effect quantum lambda calculus

There are three institutions paying for the missions:
  • Inria, for those at Inria
  • MAEDI, for all French partners but those at Inria
  • CAPES for the Brazilians partners
Please, contact your local administration in advance to demand how does it work in your case.

From Ezeiza International Airport to Buenos Aires City

The easiest way is to book the shuttle "Manuel Tienda León". There are different services:
  • Remis: Door to door service. $755 (45.30 € | 160.20 R$)
  • Bus: Bus from Ezeiza to Puerto Madero Terminal. $190 (11.40 € | 40.30 R$) + taxi to the hotel (< $100 = 6 € | 21.20 R$)
You can pre-book the service through their web page (Spanish only), or book it directly at the airport: As soon as you take your luggage, and before exiting the last door, Tienda León is at your left.

There are other companies at the airport, next to Manuel Tienda León, which may be cheaper: Those are perfectly safe options.
Just do not follow any taxi driver not booked at one of these ticket boxes.

From Buenos Aires City to Bernal

There are four options
  • Combis (Private vans)

    There is a "Combis" Station in the City Center (map)
    The ride cost $50 (3 € | 10.60 R$).
    Some info about this service (in Spanish) can be found here. (However, there is no time table nor prices in that site, only a few nice pictures of the place, sorry about that). The combis comming to Bernal depart from docks 11 and 12.
    The combis works every working day. (Attention, December 8 is holidays here and the next day is a holidays bridge).

  • Bus

    There is a direct bus, which do almost the same path as the combi. It is the 159 line marked as "B/G".
    Here you can find the full path of the line (it has a stop just at the entrance of the campus)
    The ride costs around $7.5 (0.45 € | 1.60 R$).

  • Train

    There is a direct train from Constitución Station.
    Constitución Station is the end of Subte (our "metro") C.
    Bernal station is quite close to the university
    The ride costs $2 (0.12 € | 0.42 R$).

    Safety tips: There may be pickpockets in the trains and stations, however, following the following rules is enough to avoid them:
    • Take your backpack to the front, and not the back.
    • Do not show your cellphone / kindle / laptop. Keep them hide the whole ride.

  • Taxi

    A taxi from the city center to the University may cost between $300 and $350 (18 € to 22 € | 65 R$ to 75 R$). The safest is to call it directly from the hotel.
For the train and the bus, as well as the subte (metro), you need to buy a card called "Sube", which you will recharge later. The Sube card costs $25 (1.50 € | 5.3 R$) to be paid just once, and can be recharged in any train or subte station, as well as some shops.

The University

The first two days of seminars will be held at the campus of the Universidad Nacional de Quilmes.

The address of the campus is
Roque Sáenz Peña 352, in Bernal, 15 km away from Buenos Aires city center.

The next days we will be in the University's offices informally known as "la casita de Beltrán", which is at walking distance from the campus:
Luis Beltrán 160, in Bernal.

Some suggestions:

All the suggested hotels are at a walking distance of the Terminal de Combis, Subte B and the starting point of the 159 bus.
If you chose another option, please, feel free to ask me about the hotel or the area of it before booking. Buenos Aires have some really nice areas and some areas where is better to not stay close if you are not local (similar to the "favelas" in Brazil).


Argentina currency is the peso (symbol $). There is a huge inflation right now, which means that you should not buy pesos much in advance (the longer you wait, the more pesos you will be able to buy with your euros/reals).

Right now (7-Nov-16) 1 euro is 16.66 pesos and 1 real is 4.71 pesos.

Beware that the ATM in Argentina may charge you $100 each time you withdraw money (~6 € | 21.20 R$). You can also use your bank card in many places, but not as much as in France (probably more comparable to Italy), so you will need some cash. You can change at the airport (while it is not always the best rate), or there are many exchange places at the city center. Also, you may pay with euro in some places, but they will be taken at a bad rate (and they will not have change to give you).