The Mocqua team seminar usually takes places on Thursdays at 11:00 at Loria, either in room C005 or B013. For instructions on how to reach the lab, click this link; once you're at the front desk, ask for Guilhem Gamard. Please send questions and requests about the seminar to guilhem point gamard at loria point fr.
The following links point to an automatically-updated agenda of our talks, suitable for your favorite groupware. In the summary below, all dates are YYYY/MM/DD and all times are local to Nancy (UTC+1 in Winter, UTC+2 in Summer).
English is the preferred language for all talks.
2025-05-07, 11:00:00, Room C005
Thins spans were recently introduced as a quantitative, or proof-relevant, model of programming languages based on spans of groupoids. As a model of linear logic, they can be seen as an extension of the relational model Rel where, in the interpretation of a program, not only some inputs are related to some outputs, but the different ways or computations a program can make to transform the given inputs to the given outputs are recorded.
In an ongoing work, we show that thin spans provide a useful model of so-called rigid intersection types, that are non-idempotent and non-commutative intersection types. It is already known that the relational model Rel can be syntactically described using a non-idempotent but commutative intersection type system. The commutativity is essential for the property of subject reduction, stating that the interpretation of a program is not changed by reduction. Nevertheless, the interpretation of programs in thin spans can be described by a rigid intersection type system, while still enjoying a relaxed subject reduction property.
In this talk, a rather light-weight presentation of thin spans will be given, followed by a presentation of the rigid intersection type system associated to them.
This is joint work with Pierre Clairambault
2025-03-27, 11:00:00, Room B013 (Bob)
Plane-walking automata were introduced by Salo & Törma to recognise languages of two-dimensional infinite words (subshifts), the counterpart of 4-way finite automata for two-dimensional finite words. We extend the model to allow for nondeterminism and alternation of quantifiers. We prove that the recognised subshifts form a strict subclass of sofic subshifts, and that the classes corresponding to existential and universal nondeterminism are incomparable and both larger than the deterministic class. We define a hierarchy of subshifts recognised by plane-walking automata with alternating quantifiers, which we conjecture to be strict.
2025-03-06, 14:00:00, Room B013
In 1964, R. Berger proved the existence of strongly aperiodic subshifts of finite type (SFT) on 𝕫², and used them to prove the undecidability of the Domino Problem. With the goal of understanding what aspects of 𝕫² account for this result, there has been an effort in recent years to characterize the groups with undecidable Domino Problem, and groups that admit strongly aperiodic SFTs. A key result in this direction is a result by Cohen that states that both the decidability of the Domino Problem and the existence of strongly aperiodic SFTs are quasi-isometry invariants for finitely presented groups. In this talk, I will explain how to generalize this result to new structures called blueprints. I will show how this generalizes results from the literature that use structures other than groups, and use the result to show that the Domino Problem for multidimensional geometric tilings is undecidable. This is joint work with Sebastián Barbieri.
2025-02-27, 11:00:00, Room B013
Dans cet exposé, nous présenterons les notions de catégorie fermée, de catégorie symétrique fermée et de catégorie fermée avec une famille de monades. Nous montrerons que, sous certaines conditions, elles sont essentiellement équivalentes à une logique combinatoire avec types. De plus, nous verrons un théorème de complétude fonctionnelle dans le cadre des catégories fermées avec monades.
2025-02-06, 11:00:00, Room B013
Le mot d’Oldenburger-Kolakoski (ou simplement le mot d’Oldenburger) O = 22112122122112··· étudié par R. Oldenburger (1939), puis redécouvert par W. Kolakoski (1965), est l’unique mot à la fois point fixe de l’opérateur de codage par plage et commençant par la lettre 2. Il n’est pas périodique (Oldenburger,1939), sa complexité en facteurs est bornée polynomialement (Weakley, 1989), il ne contient qu’un ensemble fini de carrés, aucun cube (Carpi, 1993 et 1994) et n’est point fixe d’aucune substitution (Carpi, 1993 et Lepistö 1993)… Néanmoins, de nombreuses conjectures et questions subsistent sur ce mot. L’une des plus fascinantes est certainement la question posée par M. S. Keane en 1991 : « La moyenne du nombre d’occurrences de la lettre 1 dans le préfixe de O tend-elle vers 1 /2 ? » Dans cet exposé, nous montrons que certaines questions ouvertes sur le mot d’Oldenburger possèdent des réponses, parfois même complètes, lorsque nous relâchons légèrement la définition du mot d’Oldenburger.
2025-01-16, 11:00:00, Room B013
A well-known feature of quantum information is that it cannot, in general, be cloned. Recently, a number of quantum-enabled information-processing tasks have demonstrated various forms of uncloneability; among these forms, piracy is an adversarial model that gives maximal power to the adversary, in controlling both a cloning-type attack, as well as the evaluation/verification stage. Here, we initiate the study of anti-piracy proof systems, which are proof systems that inherently prevent piracy attacks. We define anti-piracy proof systems, demonstrate such a proof system for an oracle problem, and also describe a candidate anti-piracy proof system for NP. We also study quantum proof systems that are cloneable and settle the famous QMA vs. QMA(2) debate in this setting. Lastly, we discuss how one can approach the QMA vs. QCMA question, by studying its cloneable variants. This is a joint work with Anne Broadbent, Supartha Podder and Jamie Sikora.
2024-12-12, 11:00:00, Room A008
Pré-soutenance de la thèse dont le résumé figure ci-dessous.
Cette thèse est consacrée à l'étude des sous-décalages, et en particulier leurs propriétés calculatoires. De façon générale, un sous-décalage est défini par un ensemble fini de symboles, un ensemble de règles spécifiant les agencements valides et invalides de ces symboles, et un espace ambiant que l'on cherche à paver: une configuration valide consiste alors en un agencement de ces symboles couvrant l'espace entier et respectant toutes les contraintes. Le sous-décalage est alors défini comme l'ensemble de toutes les configurations valides. Dans le cas le plus simple, ces règles interdisent simplement à certains symboles d'être placés côte-à-côte, et sont donc en nombre fini. Cependant, même dans ce cas restreint, les pavages de Z^d pour d > 1 sont étonnament complexes, cette complexité se manifestant sous plusieurs aspects étudiés dans cette thèse.
Cette thèse est divisée en trois chapitres essentiellement indépendants, précédés d'une introduction générale aux différents objets étudiés. Dans un premier temps, nous étudierons l'entropie d'extension des pavages de Z^d, un nombre réel associé à un sous-décalage qui quantifie le nombre de motifs qui peuvent être librement interchangés dans n'importe quelle configuration valide. Nous montrerons que les entropies d'extension possibles sont caractérisées par des restrictions calculatoires, et correspondent exactement à des niveaux de la hiérarchie arithmétique, le niveau exact dépendant de la classe de sous-décalages considérée. Dans un second chapitre, nous nous intéresserons au Groupe Fondamental Projectif des pavages du plan Z^2. Il s'agit d'un groupe associé à certains sous-décalages, qui permet de classifier les obstructions possibles qu'ont certaines configurations partielles ne pouvant être étendues en configurations valides sur tout l'espace. Nous montrerons là aussi que des classes simples de pavages, notamment les sous-décalages de type fini, peuvent exhiber un comportement complexe, et en particulier peuvent avoir comme groupe fondamental n'importe quel groupe finiment présenté. Enfin, nous étudierons dans un troisième chapitre les sous-décalages substitutifs, dans le contexte particulier des graphes. Nous proposerons une définition de graphe substitutif, et de sous-décalage substitutif défini sur ces graphes, et montrerons qu'une large classe de ces sous-décalages peuvent être obtenus à l'aide d'un nombre fini de règles locales. Ce résultat généralise partiellement un résultat classique de Mozes, dans un cadre plus combinatoire et moins géométrique.
2024-12-05, 11:00:00, Room B013
Mon objectif est de développer les bons outils (diagrammes, réécriture, formes canoniques, …) pour obtenir (ou retrouver) des présentations par générateurs et relations dans les 4 cas fondamentaux de sommes et de produits (ensemblistes et vectoriels):
* la somme ensembliste + (cas basique) ;
* la somme directe ⨁ (cas linéaire) ;
* le produit ensembliste × (cas classique) ;
* le produit tensoriel ⨂ (cas quantique).
On obtiendrait (ou retrouverait) ainsi les portes des circuits booléens classiques et quantiques, et les relations qu’elles satisfont.
2024-05-30, 11:00:00, Room B011
We provide syntax and semantics aimed at a simply-typed calculus based on pattern-matching, developed to represent quantum reversible operations, in the fashion of Sabry, Valiron and Vizzotto. To do so, a syntactic notion of orthogonal decomposition is introduced, and we show that it fits the expectations of the orthonormal basis in Hilbert spaces. A denotational semantics and an equational theory are developed, and we prove that the latter is complete with regard to the former. We later discuss how an improvement of this language is sound to represent the quantum switch. Finally, we open with conjectures on quantum recursion.
2024-04-12, 11:00:00, Room C005
Aperiodic tilesets derived from cut and project tilings
2024-04-09, 11:00:00, Room C005
Gaussian quantum mechanics is an important fragment of infinite-dimensional quantum theory, in particular for quantum optics. Calculations in Gaussian quantum mechanics often make use of an operation known as "infinite-squeezing", an operation whose mathematical description typically rests on shaky ground. Building on the previous talk, I will show how a simple modification to the symplectic ZX-calculus yields both a sound semantics and a complete ZX-calculus for Gaussian quantum mechanics with infinite-squeezing. I will then show how this new graphical language interprets previous graphical notations and languages for infinite-dimensional quantum systems.
2024-04-09, 10:00:00, Room C005
The last decade has seen the emergence of two successful research directions using drawings for reasoning on respectively dataflow in programs and quantum computations, namely Graphical Linear Algebra and ZX calculus. Taking the parallel development of those two diagrammatical approaches seriously leads to a surprising connection between quantum computing and symplectic geometry. In this talk, I will introduce the elementary symplectic notions, present a graphical language between the two research programs and outline what future developments we can expect, the final goal being a new model of quantum computation, possibly ending the reign of Hilbert spaces.
2024-04-04, 13:00:00, Room A008
Predicting the limit dynamics of automata networks (like deciding if a given network has a fixed point) is a hard problem. We would like to improve our understanding of their attractors on specific families of networks, like disjunctive networks. To do so, we decompose networks into modules, which were defined in my PhD thesis; these modules are automata networks with inputs and outputs. In this presentation we will show what has been done so far using this modular approach, including the definition of output functions (a new way of understanding a network's computation) and an equivalence to the fixed points of a family of cellular automata, culminating in the showcase of a interaction digraph transformation method that's in the works, and could help to prove the dynamical equivalence of families of networks through the transformation of their interaction digraphs.
2024-03-28, 11:00:00, Room A008
In this talk we'll prove that donuts and ping-pong balls are not the same thing. Three times. The first time with fundamental sets (a simplified version of fundamental groups of my own design), the second time with homology and the third time with cohomology. The goal is to provide as much intuition as feasible about these notions, so expect few proofs and lots of handwaving.
2024-02-22, 11:00:00, Room A008
Finite automata are one of the most basic models of computation. A sequence (uₙ)n≥0 such that un can be computed by a finite automaton with the base-k representation of n is called k-automatic sequence. On the other hand, cellular automata are dynamical systems defined by a local rule wich acts uniformly and synchronously on the configuration space.
In 2015, Eric Rowland and Reem Yassawi established a surprising close connection between these two objects. They showed that, if q is a power of a prime number, the columns of linear cellular automata are q-automatic sequences and conversly all q-automatic sequences can be realized by some linear cellular automaton with memory. Moreover, they provide a constructive method to generated a given q-automatic sequences by an explicit cellular automaton.
I will start by presenting several constructions of q-automatic sequences by linear cellular automata. Then, I will present constructions of emblematic sequences from combinatorics on words or number theory, using non-linear cellular automata with signals such as Sturmian words with a quadratic slope or the characteristic sequence of the set of integers that are sums of two squares.
2024-02-02, 10:30:00, Room C005
Evaluating and optimizing quantum computation strategies and architectures based on their energy consumption has attracted attention recently. Quantum thermodynamics provides a promising framework to do so as it formulates the fundamental constraints about energy exchanged with quantum systems. In this talk, I will provide some context about quantum thermodynamics and try to give some overview about how it could be used in the context of quantum computation and about the challenges along the way.
2024-01-25, 11:00:00, Room B013
We give complete equational theories for the props of affine Lagrangian and and affine coisotropic relations over arbitrary fields. Over odd prime fields, the prop of affine Lagrangian relations specializes the odd-prime-dimensional stabiliser fragment of ZX-calculus; and extending to affine coisotropic relations adds quantum discarding. Over fields of characteristic 0, these props give semantics for affinely constrained classical mechanical systems. Therefore, this provides a unifying theory for a subset of classical and quantum mechanical circuits. To prove completeness, we introduce a scalable notation for composite system in terms of ``spiders'' decorated by symmetric matrices. In the quantum semantics, this gives an extremely concise description of graph states; and likewise for impedance matrices in classical mechanics.
This is based on joint work with Titouan Carette and Robert I. Booth:
https://arxiv.org/abs/2401.07914
2024-01-18, 11:00:00, Room A006
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, symmetrical pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language.
2024-01-11, 11:00:00, Room B013
Penrose tilings are non-periodic tilings of the plane by two rhombuses up to isometry. Here we study dynamic percolation : a contamination process on Penrose tilings starting from a random initial configuration.
Given a Penrose tiling we put a state 0 or 1 on each tile. On these configurations we run the Boostrap percolation cellular automaton: state 1 is stable and a 0 cell becomes 1 if it has (at least) two 1 neighbors. We say that a configuration percolates when its limit configuration is 1-uniform, i.e., when running the Bootstrap percolation cellular automaton on the configuration, every tile eventually gets contaminated.
Denote B the set of configuration that percolate. We prove that for any Bernoulli measure μ (of positive parameter d) we have μ(B)=1.
In other words, for any positive parameter d, if we pick an initial configuration c at random on a Penrose tiling following a Bernoulli distribution of parameter d the probability that c percolates (every tile eventually gets contaminated) is 1.
2023-12-07, 13:15:00, Room C005
In this talk, I will summarize the results of papers [1] to [4]. In [1], we introduced the logical connective ⊙ ("sup") in Natural Deduction, which corresponds to conjunction but also adds the elimination rule for disjunction with a non-deterministic cut-elimination. Additionally, two proof terms are added: a sum and a scalar product, enabling the direct encoding of quantum algorithms using the "sup" connective to encode the quantum measurement. In [2], we showed that for the fragment without "sup" but with sum and scalar product, using linear types, linearity can be directly expressed in the proof terms: the proof t(u+v) is shown to be equivalent to t(u) + t(v), and the proof t(a∙u) is shown to be equivalent to a∙t(u). Furthermore, we prove that the "sup" connective corresponds to additive conjunction, with an elimination rule corresponding to additive disjunction. In [3], we provide a categorical model for the linear calculus without "sup" in the category SM of semimodules over a fixed commutative semiring. Finally, in [4], we show that the same category allows modelling the "sup" connective, providing an alternative for nondeterministic languages to Moggi's Powerset Monad, in contexts like the SM category where such a monad does not fit.
References: [1] A. Díaz-Caro and G. Dowek. A new connective in Natural Deduction and its application to quantum computing. Theoretical Computer Science 957:113840, 2023. [2] A. Díaz-Caro and G. Dowek. Linear Lambda-Calculus is Linear. (FSCD 2022) - LIPIcs 228:21, 2022. (Journal long version in review: arXiv:2201.11221, 2023). [3] A. Díaz-Caro and O. Malherbe. Semimodules and the (syntactically-)linear lambda calculus. Under review. arXiv:2205.02142, 2022. [4] A. Díaz-Caro and O. Malherbe. Non-determinism in a Linear Logic type discipline: A concrete categorical perspective. Under review. arXiv:2309.04624, 2023.
2023-11-23, 11:00:00, Room C005
In recent work, we have proposed a new approach for proving expectation-based properties of probabilistic programs, combining eHL, a Hoare style logic to reason about expectations, with a “hopping” proof rule incorporating a relational program logic (pRHL to be precise). The logic has recently been added to EasyCrypt, a proof assistant tailored for reasoning about relational properties of probabilistic programs. As one example application, we have formalised the proof of the logarithmic average case search complexity bound for skip lists, a simple but intricate to analyse probabilistic data structure for dicitionaries. Recently, Barbosa et al. employed the logic proving security of Dilithium, a post-quantum signature scheme recently standardized by the NIST (National Institute of Standards and Technology).
In the talk, I will give an overview of the overall approach, the case studies which were central motivations behind the approach, and, if time permits, give a short demo.
2023-10-19, 11:00:00, Room B013
Will the energy demands for large-scale quantum computers prevent their realization, or could they bring an energy advantage before a computational one? Answering this question mandates a synergy of fundamental physics and engineering: the former for the microscopic aspects of computing performance, and the latter for the energy consumption. In this work, we propose a holistic methodology dubbed Metric-Noise-Resource (MNR) able to quantify and optimize all aspects of a full-stack quantum computer, bringing together concepts from quantum physics (e.g., models of noise and quantum equation of motion), quantum information (e.g., type of quantum error correction, implementation of the algorithm at the logical level), and enabling technologies (e.g., cryogenics, control electronics, and wiring). The computer being seen as a unique physical system, our approach allows us to minimize its resource cost, acknowledging the several interdependencies between the different parts of the computer, whether they affect hardware or software.
As a proof of concept, we use MNR to minimize the power consumption of a complete model of fault-tolerant quantum computer. Comparing this with a classical supercomputer performing the same task, we identify a quantum energy advantage in regimes of parameters distinct from the commonly considered quantum computational advantage. This provides a previously overlooked practical argument for building quantum computers. While our illustration uses highly idealized parameters inspired by superconducting qubits with a specific concatenated error correction scheme, our methodology is universal -- it applies to other qubits and error-correcting codes --. It provides experimenters with guidelines to build energy-efficient quantum processors. In some regimes of high energy consumption, it can reduce this consumption by orders of magnitudes. Beyond the sole question of energy, our approach provides a framework for a multidisciplinary team of scientists aiming to establish clear roadmaps to scale up quantum computers. Overall, our multidisciplinary methodology lays the foundations for resource-efficient quantum technologies.
2023-09-22, 10:10:00, Room C005
L’objectif principal de cette thèse est d’examiner le concept de " type calculable " et d’améliorer notre compréhension globale de cette notion, ainsi que de fournir des techniques pour vérifier ou réfuter cette propriété. Un espace métrisable compact est dit de type calculable si pour tout ensemble homéomorphe à cet espace, semi-calculabilité et calculabilité sont équivalentes. Cette étude s’appuie sur les travaux de Miller, qui a démontré que les sphères de dimension finie sont de type calculable, ainsi que sur les travaux d’Iljazović et d’autres auteurs, qui ont étendu cette propriété à divers espaces tels que les variétés compactes.
Pour commencer, nous établissons l’équivalence entre deux définitions distinctes de type calculable présentes dans la littérature, impliquant respectivement des espaces métriques et des espaces de Hausdorff. Nous soutenons que la version relativisée et plus forte du type calculable présente des propriétés plus favorables et se prête bien à l’analyse topologique. Nous obtenons ainsi des caractérisations du " type calculable fort " de nature purement topologiques, et en lien avec la complexité descriptive des invariants topologiques.
Cela nous amène naturellement à notre deuxième objectif, l’étude du pouvoir expressif des invariants topologiques de faible complexité descriptive et de leur capacité à distinguer des espaces différents. Plus précisément, nous étudions deux familles d’invariants topologiques de faible complexité qui capturent l’extensibilité et la trivialité homotopique des fonctions continues. En utilisant ce cadre, nous revisitons les résultats précédents sur le type calculable et découvrons de nouvelles perspectives. Notamment, nous identifions la complexité du problème de séparation des graphes topologiques finis.
Enfin, notre troisième objectif se concentre sur l’application de la théorie de l’homologie à l’étude de ce que nous appelons la " propriété de surjection " , qui caractérise la propriété de type calculable. Par exemple, nous prouvons qu’un complexe simplicial fini est de type calculable (fort) si et seulement si l’étoile de chaque sommet satisfait la propriété de surjection. De plus, la réduction à l’homologie implique que la propriété de type calculable est décidable pour les complexes simpliciaux finis de dimension au plus 4.
2023-06-22, 11:00:00, Room C005
Let s(n) denote the sum of digits in the binary expansion of the integer n. Hare, Laishram and Stoll (2011) studied the number of odd integers such that s(n) = s(n2) = k, for a given positive integer k. The remaining cases that could not be treated by theses authors were k = 9, 10, 11, 14 or 15. In this talk, I will present the results of our article on the cases k = 9, 10 and 11 and the difficulties to settle for the two remaining cases k = 14 and 15. A related problem is to study perfect squares of odd integers with four binary digits. Bennett, Bugeaud and Mignotte (2012) proved that there are only finitely many solutions and conjectured that the set of solutions is composed of 13, 15, 47 and 111. In the same paper, we give an algorithm to find all solutions with fixed sum of digits value, supporting this conjecture, as well as show related results for perfect squares of odd integers with five binary digits. This is joint work with Aloui, Jamet, Kaneko, Kopecki and Stoll.
2023-06-12, 14:00:00, Room C005
The study of pattern-avoiding inversion sequences began in two independent articles by Mansour–Shattuck and Corteel–Martinez–Savage–Weselcouch in 2015 and 2016. Subsequent works (by Lin–Yan, Martinez–Savage, and Mansour–Yildirim among others) left their enumeration open for only one single pattern, and 23 pairs of patterns of length 3. We solve all of those remaining cases by finding recurrence formulas (as well as a few closed formulas), using four different decompositions of pattern-avoiding inversion sequences. These formulas allow us to compute between 100 and 350 terms of each enumeration sequence in one minute, using C++ programs running on a personal computer.
2023-05-11, 10:00:00, Room B011
The classical computational complexity of counting on the one hand and quantum computing on the other hand at first glance seem disconnected. Yet techniques from quantum computing, particularly from graphical languages, are very useful in reasoning about counting complexity. In this talk, I will discuss both existing results and some ongoing work that connects a classical family of counting problems called holant to quantum computing.
2023-03-09, 11:00:00, Room B013
In the average-case analysis of algorithms working on arrays of numbers (modeled by permutations), the uniform distribution on the set of possible inputs is usually assumed. However, the actual data on which these algorithms are used is rarely uniform, and often displays a bias towards "sortedness". In this talk, we present a non-uniform distribution on permutations, which favors their records (a.k.a. left-to-right maxima). We describe the behavior (on average and in distribution) of some classical permutation statistics in this model, some of which with applications to the analysis of algorithms. We also describe the "typical shape" of permutations in our model, by means of their (deterministic) permuton limit.
This is joint work with Nicolas Auger, Cyril Nicaud and Carine Pivoteau.
2023-02-16, 11:00:00, Room Room B013
We propose a new framework for structured prediction based on machine learning algorithms that optimise over classes of functors rather than functions. This functorial learning approach was at the basis of the recent development of quantum natural language processing (QNLP), where we learn functors from formal grammars to parameterised quantum circuits. In order to find optimal functors efficiently, we introduce diagrammatic differentiation: a graphical language to compute the gradients of quantum circuits and string diagrams in general. We then discuss how to apply the same approach to learn distributed quantum protocols from their specification.
2023-02-09, 11:00:00, Room B011
La suite d’Oldenburger-Kolakoski est l’unique suite infinie sur l’alphabet {1,2} qui commence par un 1 et est un point fixe de l’application de codage par plage. Dans cet exposé, nous prendrons un peu de recul par rapport à cette suite bien connue et très étudiée, en introduisant de l’aléa dans le choix des lettres écrites. Cela nous permettra de montrer des résultats portant sur la convergence de la densité de 1 dans les suites ainsi construites. Dans le cas où les lettres sont choisies selon une suite i.i.d. de variables aléatoires ou selon une chaîne de Markov, la densité moyenne de 1 converge. De plus, dans le cas i.i.d., nous arrivons même à démontrer que la densité converge presque sûrement. Il s’agit d’un travail réalisé conjointement par Chloé Boisson, Damien Jamet, et Irène Marcovici.
2023-02-02, 11:00:00, Room B013
La mécanique quantique nous indique qu'il est fondamentalement impossible d'extraire de l'information d'un état quantique sans l'altérer… et parfois certaines propriétés sont même impossibles à extraire à partir d'une seule copie, y compris en mesurant notre qubit de manière destructive. On pourrait donc penser qu'il est impossible de vérifier, en recevant un étant quantique, si cet état possède certaines propriétés avancées sans le détruire. Ceci pose un vrai problème en cryptographie, où on souhaite souvent vérifier que l'état reçu a été honnêtement préparé : pour palier ce problème, des méthodes dites de cut-and-choose doivent souvent être employées, menant à une analyse de sécurité complexe et un protocole peu efficace. Nous avons montré dans un précédent article (arXiv:2104.04742) que cette intuition est erronée : en changeant substantiellement la procédure de transmission d'un état quantique, il est possible de prouver des propriétés extrêmement avancées sur un état quantique reçu, et ce sans l'altérer, de manière similaire aux protocoles Zero-Knowledge (ZK) classiques. Cependant, cette approche, basée sur la cryptographie post-quantique, est très coûteuse à implémenter et la sécurité obtenue est calculatoire. Dans cette présentation d'un travail en cours, je montrerai qu'il est possible d'obtenir à partir de méthodes complètement différentes un protocole NIZK sur un langage quantique plus simple, mais de manière plus efficace et plus sécurisé (sécurité inconditionnelle sous certaines conditions). Je montrerai également les applications au calcul multipartite, en fournissant un protocole d'Oblivious Transfer quantique plus simple, plus sécurisé, plus rapide (communication optimale), et avec une preuve de sécurité plus simple et modulaire.
2023-01-26, 11:00:00, Room C005
Comment empiler un nombre infini d'oranges pour maximiser la proportion de l'espace couvert ? Kepler a conjecturé que l'empilement des "balles de canon" est optimal. 400 ans se sont écoulés avant que cette conjecture soit démontrée par Hales et Ferguson dont la preuve comporte 6 papiers et plus de 50000 lignes de code. Comment arranger un nombre infini de pièces de monnaie de 3 rayons différents sur une table infinie pour maximiser la proportion de la surface couverte ? Un arrangement de disques est dit triangulé si chacun de ses "trous" est borné par trois disques tangents. Connelly a conjecturé que si de tels arrangements existent, l'un d'eux maximise la proportion de la surface couverte. Nous avons démontré cette assertion pour 31 triplets de rayons de disques et l'avons réfuté pour 40 autres triplets. Je vais vous présenter nos résultats sur les arrangements triangulés à 3 disques et les analogies entre notre preuve et celle de la conjecture de Kepler.
2023-01-19, 11:00:00, Room B013
Over the past decade, a number of quantum processes have been proposed which are logically consistent, yet feature a cyclic causal structure. However, there exists no general formal method to construct a process with an exotic causal structure in a way that ensures, and makes clear why, it is consistent. Here we provide such a method, given by an extended circuit formalism. This only requires directed graphs endowed with boolean matrices, which encode basic constraints on operations. Our framework (a) defines a set of elementary rules for checking the validity of any such graph, (b) provides a way of constructing consistent processes as a circuit from valid graphs, and (c) yields an intuitive interpretation of the causal relations within a process and an explanation of why they do not lead to inconsistencies. We display how several standard examples of exotic processes, including ones that violate causal inequalities, are among the class of processes that can be generated in this way; we conjecture that this class in fact includes all unitarily extendible processes.
2023-01-12, 11:00:00, Room C005
We explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a PROP to model computation in this framework, where the choice is parametrized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition. The graphical language comes equipped with a denotational semantics based on linear applications and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to the semantics.
2022-12-07, 11:00:00, Room C005
We introduce the first complete equational theory for quantum circuits. More precisely, we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations. The proof is based on the properties of multi-controlled gates – that are defined using elementary gates – together with an encoding of quantum circuits into linear optical circuits, which have been proved to have a complete axiomatisation. This is a joint work with Alexandre Clément, Nicolas Heurtel, Shane Mansfield, and Benoît Valiron.
2022-10-27, 14:00:00, Room B011
We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first programming language-based characterization of the quantum complexity class FBQP. Finally, we present a tractable semantics-preserving algorithm compiling each PFOQ program to a quantum circuit of size polynomial in the number of input qubits.
2022-10-06, 11:00:00, Room B013
An automata network is a graph where each node is a finite-state machine. The vertices of the graph should be thought as computers with very limited memory and the edges as network links. Each machine has its own transition table and possibly its own set of states. There is no input of any kind: the machines read the current states of their neighbors in the graph, and use those states (all concatenated) as input symbols. The system runs in rounds and, in my research line, all machines are updated simultaneously in each round. (In other terms this is similar to a cellular automaton, except that the “grid” is an arbitrary graph and there is no uniformity: different cells have different update functions.)
An automata network is usually given as a couple (G,f_v), where G is the graph and (f_v) is a family of Boolean circuits indexed by the vertices of G. The circuit f_v encodes the update fonction of the node v, so updating a node is the same as evaluating a Boolean circuit.
I'll state and give a few proof elements of general complexity results on automata networks. More precisely: if we focus on deterministic networks, then any question expressible in first-order logic on a given signature is either O(1), or NP-hard, or coNP-hard. On the other hand, if we focus on nondeterministic networks, then a large class of questions expressible in MSO logic on a given signature is either O(1), or NP-hard, or coNP-hard.
The intuition behind these results is that there is no hope to “parse” the Boolean circuits of an automata network to try and infer something about its general behavior.