CAPP - Quantum and Classical Computation

CAPP: Calculus, Algorithm, Programs and Proofs

The CAPP team carries out research in theoretical computer science, especially in the fields of rewriting, logic, automated reasoning, and quantum computing. We devise formalisms, algorithms, and tools for the specification, design, analysis, and certification of complex computing systems.

Motivations

Computing devices are becoming increasingly numerous, heterogeneous, and complex, with most human activities now relying on them. In this context, errors or malfunctions can lead to dramatic consequences, ranging from significant financial losses to human casualties, or more subtle issues such as incorrect or inappropriate decisions. It is therefore crucial to simplify and rigorize the development of these systems and to ensure their correct behavior. Additionally, equipping computing devices with reasoning capabilities allows them to extract explicit knowledge from their environment, provide convincing justifications for their decisions, interact with other agents, and more. The CAPP team develops theoretical tools and results to tackle these challenges.

Research Program

We design high-level languages to describe computations, tailored to various application domains and grounded in solid theoretical foundations, such as rewriting, logic, or category theory. We analyze the properties of these models for information processing, define logics to specify and verify computation properties, and study their expressivity and computability. We also develop automated reasoning procedures, implement them as research prototypes, and apply them to solve real-world problems. Here, reasoning encompasses a broad scope: not only proving valid properties but also extracting knowledge through tasks like data analysis, synthesizing explanations, filling in missing information, and transforming proofs.

Part of the team is dedicated to quantum computing, a pivotal challenge at the intersection of computer science and physics. Quantum computing leverages phenomena such as superposition and entanglement to perform computations (e.g., a quantum bit can exist in a superposition of 0 and 1 with certain probabilities). These phenomena enable algorithms that surpass the speed of classical counterparts, offering transformative potential for computational efficiency.

Topics

• Quantum Computing (Contact: M. Mhalla)
  • Error correction for quantum information
  • Quantum control of quantum circuits
  • Erasure of quantum information
  • Incompatibility of quantum measurements
  • Quantum entropies
• Automated Reasoning (Contact: N. Peltier)
  • Separation logic
  • Inductive reasoning
  • Superposition calculus
  • Formalization of financial mathematics
• Rule-based Programming (Contact: R. Echahed)
  • High-level frameworks for graph transformation
  • Parallel graph rewriting
  • Verification of graph transformations

Grants

We are or were partners of the following grants:

• ANR project BlockFi: Blockchain et Finance Décentralisée (PI: E. Gobet, local coordinator: M. Echenim, 24-29).
• PEPR ANR project – EPiQ (22-27): Etude de la pile quantique : Algorithmes, modèles de calcul et simulation pour l’informatique quantique (local coordinator: M. Echenim).
• IRGA project – POQIT (23-24) – Non-commutative polynomial optimization methods for quantum information theory (PI: A. Bluhm).
• ANR project VerifGraph (22-26): Verifiable Graph Queries and Transformations, R. Echahed, with Leonid Libkin (head) and Angela Bonifati.
• ANR project NARCO (22-26): Non-Aggregative Resource COmpositions (PI: N.Peltier, partners: LIG, LMF, LORIA, Verimag).
• UGA IRGA project SLIDD (21-24). Separation Logic with Inductive Definitions and Data (N. Peltier, with R. Iosif, Verimag).
• LIG project “Emergence”. Graph Rewriting for Quantum Computing (2020-2021, N. Peltier).
• LIG project “Emergence” Réécriture Parallèle (2019-2020, T. Boy de la Tour)
• LIG project “Emergence” Abductive Reasoning and Separation Logic (2018-2019, heads: M. Echenim and N. Peltier)
• ANR project ASAP (PI: A. Leistch and N. Peltier)
• ANR project CLIMT (PI: R. Echahed).
• ANR project GAG.

Systems

• Slipshow. An engine for displaying an enhanced version of slides (called slips). See the documentation. Developed by Paul-Elliot Anglès d’Auriac.
• GPID: abduction modulo theories (part of the Abdulot framework). Implemented by Y. Sellami.
• Ilinva: a system to generate loop invariants (uses GPID and Why3). Implemented by Y. Sellami.
• DEI: theorem proving with iterated terms. Implemented by H. Bensaid.
• FISH: A Flat Instantiation ScHeme.

Publications

You can obtain all publications of the CAPP team on HAL

Major Events

• February 25. I. Šupić (CR CNRS) joined CAPP.
• September 24. Start of the BlockFi ANR project.
• November 22. A. Bluhm (CR CNRS) joined CAPP.
• January 22. Kesitys is now part of Kaiko.
• January 22. Start of the NARCO project (ANR).
• January 22. Start of the EPiQ project (ANR, Etude de la pile quantique: Algorithmes, modèles de calcul et simulation pour l’informatique quantique).
• October 21. Start of the VeriGraph project (ANR).
• December 2020. Alastair A. Abbott (CR Inria) is hosted by the CAPP team.
• IJCAR 2020: International Joint Conference of Automated Reasoning (co-PC-chair: N. Peltier)
• Start of the “LIG TIC Talks” (organized by F. Prost)
• July 2019. Rachid Echahed co-chaired (with D. Plump) the 10th International Workshop on Graph Computation Models.
• July 2019. Rachid Echahed gave a lecture “Introduction to Graph Rewriting” at the 11th International School on Rewriting (ISR 2019)
• April 29-30 2019: Informal workshop on Separation Logic in Paris (organized by R. Iosif, Verimag).
• February 25-26, 2019: First workshop on ZX calculus.
• February 2019: N. Peltier replaced R. Echahed as the head of the CAPP team.
• End 2018: creation of the Kesitys start-up, co-founded by M. Echenim (CAPP), Emmanuel Gobet and Anne-Claire Jeancolas.

Seminars (non exhaustive)

• April 29, 2025. Mehdi Mhalla is defending his habilitation thesis. Discrete tools for understanding quantum information (10 am, IMAG Amphitheater).
• January 7. Kick-off meeting of the BlockFi ANR project (Blockchain et Finance Décentralisée, PI: E. Gobet local leader: M. Echenim).
• December 11-12. 6th NARCO meeting.
• December 4, 2024, 4 pm. Talk by Jacopo Surace.
• November 4, 2024. PhD Defense, Julien du Crest, Efficient Message-Passing Decoding of Quantum LDPC Codes
• May 29, 2024. Workshop MFML/LIG. Talks by P. Pocreau (Quantum query complexity of Boolean functions under indefinite causal order) and R. Echahed (Verifying Graph Transformation Systems with Description Logics)
• April 16-17, 2024. A. Leistch, A. Lolic and S. Mahler are visiting CAPP. Talks by Alex, Nicolas and Stella.
• March 13, 2024. Fifth meeting of the ANR project NARCO (10h30-17h, Paris).
• January 24 2024. Seminar by Michael Jabbour (Université libre de Bruxelles). Tightening continuity bounds on entropies and bounds on quantum capacities. IMAG 306. 2 pm.
• January 23 2024. Seminar by Leo Colisson. “How to Achieve Round-Optimal Quantum Oblivious Transfer and Zero-Knowledge Proofs on Quantum States without structure.” IMAG 482. 10:15 am.
• December 1 2023. Seminar by Radu Iosif. 1:30 pm, IMAG 482.
• November 28 2023. Seminar by Alexandre Clément. “Complete Equational Theories for Quantum circuits”. IMAG 482. 2 pm.
• November 23 2023. Séminaire LIS (Laboratoire d’Informatique et Systèmes), Demi Journée du Pôle Calcul.
• July 4 2023. iQbricks: Integration of a fully-featured quantum language in the framework Qbricks. Tomas Carneiro, IMAG 482. 1:30 pm.
• June 22 2023. Fourth meeting of the ANR project NARCO (10h30-17h, Paris).
• May 11 2023. MFML (LIG research axis) Workshop at Inria. Presentations by A. Bluhm and N. Peltier.
• April 24 2023. The paper “A Strict Constrained Superposition Calculus for Graphs” was presented at FoSSaCS (slides).
• January 25 2023. Improving social welfare in non-cooperative games with different types of quantum resources. Pierre Pocreau (CAPP/QInfo). IMAG 406, 2 pm.
• December 8 2022. Third plenary meeting of the ANR project NARCO (10h30-17h, IRIF, Paris).
  
• November 30 2022. A sublinear-time quantum algorithm for approximating partition functions. Yassine Hamoudi (Université de Berkeley). IMAG Room 406. 13h.
• November 7-9 2022. TIME 2022.
• September 21 2022. QuantAlps seminar. A Complete Equational Theory for Quantum Circuits. S. Perdrix. IMAG Room 406. 3:30 pm.
• July 31 2022. ASL (Workshop on Advancing Separation Logics).
• July 7 2022. Second plenary meeting of the ANR project NARCO (10h30-17h, IRIF, Paris).
• May 5 2022. MFML (LIG research axis) Workshop. Presentations by. T. Boy de la Tour and M. Mhalla/M. Echenim.
• March 7 2022. R. East will defend his PhD thesis. “Formal Diagrammatic Spin Physics”. IMAG building, auditorium. 2pm.
• March 2 2022. QuantAlps seminar (Quantum Information & Computing). Free spectrahedra and quantum information theory. Andreas Bluhm (University of Copenahgen).
  February 11 2022. Kick-off meeting ANR project NARCO.
  
• December 8 2021. QuEnG Quantum Computing seminar. Titouan Carette. Causality and post-selection in quantum streams. 2 pm. IMAG 482.
  
• November 24 2021. QuEnG Quantum Computing Seminar. Ravi Kunjwal. Contextuality in entanglement-assisted one-shot classical communication. 3 pm, IMAG 406 + zoom.
• October 25 2021. Quantum Polar Codes. Ashutosh Goswami. PhD defence. IMAG seminar room. 14:00.
• September 15 2021. Non-Destructive Zero-Knowledge Proofs on Quantum States, and Multi-Party Generation of Authorized Hidden GHZ States. Léo COLISSON. 15h. room 406 + Zoom.
• July 15 2021. Mehdi Mhalla. Quantum coherent control with Polarised Beam Splitters. 14h. room 482 and/or zoom.
  
• June 30 2021. Thierry Boy de la Tour. Monographes. 10:30, room 482.
• April 28 2021. Mnacho Echenim. Projective Measurements and the CHSH inequality with Isabelle/HOL. 2 pm.
  
• April 16 2021. Étienne Miquey. Environments & CPS translations, a well-typed story. 10h30.
• April 14 2021. Frédéric Holweck. Quantum contextuality: From the symplectic polar space to the IBM Quantum Experience. 2 pm.
• April 02 2021. Christophe Crespelle. Graph editing problems: algorithmic approaches and experimental results on real-world complex networks. 02:00 PM.
  
• March 31 2021. Giuseppe Di Molfetta. Gauge-invariance in classical and quantum cellular automata and multi-scales analysis. 04:00 PM.
• March 24 2021. QuEng Seminar. Mischa Woods. Covariant Quantum Error Correcting Codes via Reference Frames. 03:00 PM.
• March 10 2021. QuEng Seminar. AKLT-states as ZX-diagrams: diagrammatic reasoning for quantum states, by R. East.
• December 9 2020. CAPP meeting. Seminar by N. Peltier (14h, Zoom). About the Complexity of Decidable Entailments in Separation Logic with Inductive Definitions’.
• November 17 2020. Seminar by Paul-Elliot Anglès d’Auriac (9h, Zoom). Liens entre calcul et logique : aléatoire algorithmique et mathématiques à rebours.
  
• October 15 2020. WAX LIG Workshop, (recorded) talks by M. Mhalla (Quantum Computing) and N. Peltier (Separation Logic).
• July 8, 2020. Trimming Decoding of Color Codes over the Quantum Erasure Channel, by Sangjun Lee. 14:00.
• June 23, 2020. Yanis Sellami is defending his thesis. Raisonnement abductif modulo des théories et application à la vérification de programmes (2 pm, IMAG 447). Due to the COVID-19 pandemic, the defense is unfortunately not public.
  
• February 26, 2020. Seminar Christophe Vuillot (Codes quantiques).
• January 30, 2020. Seminar Alastair Abbott: Communication through coherently controlled quantum channels (14:00, room 482).
• January 22, 2020. Seminar Renaud Vilmart: Completeness of the ZX-Calculus for Quantum Computing (14:00, room 482).
• December 12, 2019. CAPP meeting (14:00, room 482, IMAG) on parallel graph rewriting (part III, talk by Thierry Boy de la Tour).
  
• November 25, 2019. CAPP meeting (9:00, room 482) on parallel graph rewriting (part II, talk by Thierry Boy de la Tour).
• November 21, 2019, Sophie Tourret (former CAPP member) gave a seminar at Verimag.
• October 21, 2019. CAPP meeting (8:45, room 482) on parallel graph rewriting (talk by Thierry Boy de la Tour).
• October 9, 2019. Alex Bredariol Grilo (CWI and QuSoft) gave a talk on “Stoquastic PCP vs. Randomness” (14:00, Room 406, IMAG Building).
• July 10, 2019. Ashutosh Goswami gave a presentation on quantum polar codes (14:00, Room 482, IMAG Building).
• July 8, 2019. Julian Wechs spoke about the “existence of noncausal processes on time-delocalized systems” (14:00, Room 482, IMAG Building).
• June 13, 2019. Mehdi Mhalla gave a seminar in the LIG POLARIS team about “Using quantum information to improve social welfare”.
• May 22 2019: Seminar on Categorical Quantum Dynamics by Stefano Gogioso, from the University of Oxford (IMAG Building 406).
• May 13 2019: CAPP meeting on the pushback pushout (PBPO) approach in graph transformation (talk by R. Echahed).
• April 15 2019: CAPP meeting on Separation Logic (talks by N. Peltier, N. Amat).

Some Recent Papers

• April 2025
  • The paper "A Direct Procedure to Test Entailment in a Separation Logic of Relations" by M. Echenim and N. Peltier is accepted for publication at the Journal of Automated Reasoning
  • The paper "Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting" by Qi Qiu is accepted at ICGT 2025

• January 2025
  • The paper Algebraic properties and transformations of monographs by T. Boy de la Tour appeared in Theoretical Computer Science
  • The paper Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates, by M. Echenim and N. Peltier is accepted at Fundamenta Informaticae

• August 2024
  • The paper Symbolic Graph Query Solving by Dominique Duval and Rachid Echahed was presented at SCSS

• July 2024
  • The paper Categories of Algebraic Rewrite Rules by Thierry Boy de la Tour was presented at WADT

• May 2024
  • The paper “Vertex-minor universal graphs for generating entangled quantum subsystems” by Maxime Cautrès, Nathan Claudet, Mehdi Mhalla, Simon Perdrix, Valentin Savin and Stéphan Thomassé is accepted at ICALP.
  • The paper “Some techniques for reasoning automatically on co-inductive data structures” by N. Peltier appeared in the Journal of Logic and Computation.

• April 2024
  • The paper “An EXPTIME-complete entailment problem in separation logic” by N. Peltier is accepted at Wollic 2024.
  • The paper “What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? ” by Tanguy Bozec, Nicolas Peltier, Quentin Petitjean and Mihaela Sighireanu is accepted at IJCAR 2024.
  • The paper “Subsumptions of SPO Rules” by T. Boy de la Tour was presented at TERMGRAPH 2024.

• November 2023
  • A. Bluhm has three talks accepted at 27th Annual Conference on Quantum Information Processing (QIP 2024), which is the premier conference in the field (acceptance rate around 20%).
    • “Towards a unification of different measures of correlations and locality in Gibbs states” (Andreas Bluhm, Ángela Capel, Massimo Moscolari, Antonio Pérez Hernández, Stefan Teufel and Tom Wessel).
    • “Going Beyond Gadgets: The Importance of Scalability for Analogue Quantum Simulators” (Dylan Harley, Ishaun Datta, Frederik Ravn Klausen, Andreas Bluhm, Daniel Stilck França, Albert Werner and Matthias Christandl).
    • “Making Existing Quantum Position Verification Protocols Secure Against Arbitrary Transmission Loss” (Rene Allerstorfer, Andreas Bluhm, Harry Buhrman, Matthias Christandl, Llorenc Escola Farras, Florian Speelman and Philip Verduyn Lunel)

September 2023

• The papers Layered Decoding of Quantum LDPC Codes by Julien Du Crest, Francisco Garcia-Herrero, Mehdi Mhalla, Valentin Savin and Javier Valls, and Improved Rate Fault-Tolerant Preparation of Q1 Code-States by by Ashutosh Goswami, Mehdi Mhalla and Valentin Savin, are accepted at ISTC 2023.

August 2023

• The paper “A Proof Procedure For Separation Logic With Inductive Definitions and Data” by M. Echenim and N. Peltier is accepted for publication in the Journal of Automated Reasoning.

July 2023

• The paper “Testing the Satisfiability of Formulas in Separation Logic with Permissions“ by N. Peltier is accepted at TABLEAUX 2023. Slides of the talk (on September 20).

June 2023

• The paper “Subsumptions of Algebraic Rewrite Rules” by Thierry Boy de la Tour is accepted at ACT 2023.

May 2023

• The paper “Query Complexity of Boolean Functions under Indefinite Causal Order” by Alastair Abbott, Mehdi Mhalla and Pierre Pocreau is accepted for presentation at QPL 2023.
  
• The paper “A Rule-Based Procedure for Graph Query Solving” by Dominique Duval, Rachid Echahed and Frederic Prost is accepted at ICGT 23.

January 2023

• The paper “”An Undecidability Result for Separation Logic With Theory Reasoning” by M. Echenim and N. Peltier is accepted for publication in Information Processing Letters.

December 2022

• The paper “A Strict Constrained Superposition Calculus for Graphs” by Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, and Nicolas Peltier is accepted at FoSSaCS 2023.

Members

Scientific Leader

• Nicolas Peltier (CNRS Researcher, HdR)
  Office: 481, Phone: 04 57 42 14 90
  Email: nicolas.peltier@imag.fr

Permanent Members

• Andreas Bluhm (CNRS Researcher)
  Office: 486, Email: Andreas.Bluhm@univ-grenoble-alpes.fr
• Thierry Boy de la Tour (CNRS Researcher)
  Office: 482, Phone: 04 57 42 14 62
  Email: thierry.boy-de-la-tour@imag.fr
• Mnacho Echenim (Professor GINP)
  Office: 486, Phone: 04 57 42 14 91
  Email: mnacho.echenim@imag.fr
• Rachid Echahed (CNRS Researcher, HdR)
  Office: 480, Phone: 04 57 42 15 40
  Email: rachid.echahed@imag.fr
• Mehdi Mhalla (CNRS Researcher, HdR)
  Office: 484, Phone: 04 57 42 15 30
  Email: mehdi.mhalla@imag.fr
• François Puitg (associate lecturer UGA)
  Office: 483, Phone: 04 57 42 15 46
  Email: francois.puitg@imag.fr
• Ivan Šupić (CNRS Researcher)
  Office: 480, Phone: 04 57 42 15 40
  Email: ivan.supic@univ-grenoble-alpes.fr

Non Permanent Members

• Qi Qiu (ATER, temporary teaching and research associate)
  Office: 494
  
• Christopher Spinrath (post-doctoral researcher)
  Office: 494
  

PhD Students

• Tomas Barros Carneiro
  
• Laure Cerutti
  
• Simon Hofer
  
• Raphael Le Bihan
  
• Pierre Pocreau
  

Former Members

• Paul-Elliot Anglès d’Auriac
• Julien Du Crest
• Richard East
• Ashutosh Goswami
• Frédéric Prost (MdC INSA Lyon)
• Yanis Sellami (CEA)
• Sophie Tourret (INRIA Researcher, Nancy)
• Julian Wechs

Venue

Address:

CAPP – Laboratoire LIG

Bâtiment IMAG – 150 place du Torrent

Domaine universitaire de Saint Martin d’Hères

38400 Saint Martin d’Hères

FRANCE

Scientific Head: Nicolas Peltier

Tél. : (+33) 4 57 42 15 40

Venue:

Our building is located at the center of the campus (domaine universitaire) close to the tramway station “Gabriel Fauré” on line B. Tramways reach the campus from Grenoble railway station (or bus station) in approx. 15 mn. The tramway station “Gares” is shared between lines A and B, so make sure to take a tramway with a green sign reading: “B – Gières Plaine des sports”. Tickets are sold by machines at every station, and should be validated before the trip.

Links

• Some international journals in our field of research
  • Quantum Information & Computation
  • Quantum
  • Theoretical Computer Science
  • Journal of Automated Reasoning
  • Journal of Logic and Computation
  • Fundamenta Informaticae

• Some international conferences
  • Quantum information processing
  • International Colloquium on Automata, Languages and Programming (ICALP)
  International Joint Conference on Automated Reasoning (IJCAR)
  • International Conference on Automated Deduction (CADE)
  • International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)
  • International Conference on Graph Transformation (ICGT)

• Some relevant Wikipedia articles
  • Computer Science
  • Declarative Programming
  • Automated Theorem Proving
  • Quantum Computing