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-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.