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 (head: 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 (head: N.Peltier, partners: LIG, LMF, LORIA, Verimag).
• UGA IRGA project SLIDD (21-24). Separation Logic with Inductive Definitions and Data (head: N. Peltier, with R. Iosif, Verimag).
• LIG project “Emergence”. Graph Rewriting for Quantum Computing (2020-2021, head: N. Peltier).
• LIG project “Emergence” Réécriture Parallèle (2019-2020, head: T. Boy de la Tour)
• LIG project “Emergence” Abductive Reasoning and Separation Logic (2018-2019, heads: M. Echenim et N. Peltier)
• The ANR project ASAP (head: A. Leistch and N. Peltier)
• The ANR project CLIMT (head: R. Echahed).
• The 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.
• CsP: superposition-based abduction (by S. Tourret).
• 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.
• RegSTAB: a SAT-Solver extended with the possibility to handle formulae patterns. Implemented by V. Aravantinos.

Publications

You can obtain all publications of the CAPP team on HAL

Major Events

• 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)

• 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

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

August 2022

• The paper “Reasoning on Dynamic Transformations of Symbolic Heaps” (by N. Peltier) is accepted at TIME 2022 (29th International Symposium on Temporal Representation and Reasoning). slides.

June 2022

• The paper “Two Results on Separation Logic With Theory Reasoning” (by M. Echenim and N. Peltier) is accepted for presentation at ASL 2022 (Workshop on Advancing Separation Logic).

September 2021

• The paper A Superposition-Based Calculus for Diagrammatic Reasoning by Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier was presented at PPDP 2021 (by N. Peltier). video.

July 2021

• The paper Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules by Mnacho Echenim, Radu Iosif and Nicolas Peltier has been accepted for publication in Information Processing Letters.
• The paper A Superposition-Based Calculus for Diagrammatic Reasoning by Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier is accepted at PPDP 2021.
• The paper Coherent control and distinguishability of quantum channels via PBS-diagrams (Cyril Branciard, Alexandre Clément, Mehdi Mhalla, Simon Perdrix) is accepted at MFCS’21.
• Quantum Polarization of Qudit Channels. Ashutosh Goswami, Mehdi Mhalla, Valentin Savin. ISIT 2021.

April 2021

• The paper “Unifying Decidable Entailments in Separation Logic with Inductive Definitions” by Mnacho Echenim, Radu Iosif and Nicolas Peltier is accepted at CADE 2021.

February 2021

• The final version of the paper “Parallel Independence in Attributed Graph Rewriting” by Thierry Boy de La Tour is accepted for publication in the Electronic Proceedings in Theoretical Computer Science (TERMGRAPH 2020).

January 2021

• The paper “Decidable Entailments in Separation Logic with Inductive Definitions: Beyond establishment” by M. Echenim, R. Iosif and N. Peltier was presented at CSL 2021 (recorded presentation by N. Peltier, see the video).
• The paper Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard was presented at LPAR 2020-2021 (by R. Iosif, see the slides).

December 2020

• The paper “Parallel rewriting of attributed graphs“, by R. Echahed and T. Boy de la Tour, appeared in Theoretical Computer Science.

September 2020

• The paper “Decidable Entailments in Separation Logic with Inductive Definitions” by M. Echenim, R. Iosif and N. Peltier is accepted for publication at CSL 2021 (the conference will be virtual).

July 2020

• The paper “Parallel Independence in Attributed Graph Rewriting” by Thierry Boy de La Tour is accepted for presentation at TERMGRAPH 2020.

May 2020

• The book “A Guided Tour of Artificial Intelligence Research” is now published.
• The paper “How Quantum Information can improve Social Welfare”, by Berry Groisman, Michael Mc Gettrick, Mehdi Mhalla, Marcin Pawlowski is accepted for publication in the IEEE Journal on Selected Areas in Information Theory.
• The paper “Contextuality and Expressivity of Non-locality” by Mehdi Mhalla and Sacha Huriot will be presented at QPL 2020.

April 2020:

• The paper ” Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard” (by M. Echenim, R. Iosif and N. Peltier) is accepted at LPAR 2020 (the conference is cancelled due to the COVID-19 crisis, but the proceedings will be published as usual).
• The paper “Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL” by M. Echenim, H. Guiol and N. Peltier appeared in the Journal of Automated Reasoning.
• The paper “Combining Parallel Graph Rewriting and Quotient Graphs” by Thierry Boy de La Tour and Rachid Echahed, is accepted for presentation at the 13th internation workshop on rewriting logic and its applications.

February 2020:

• The paper Combining Induction and Saturation-Based Theorem Proving (by M. Echenim and N. Peltier) appeared in the Journal of Automated Reasoning.

January 2020

• The paper “The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions” by M. Echenim, R. Iosif and N. Peltier was presented at the workshop ADSL 2020.

December 2019:

• The paper “The Bernays-Schoenfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates” by M. Echenim, R. Iosif and N. Peltier has been accepted for publication in the Transactions on Computational Logic.

November 2019:

• The paper “Algebraic graph rewriting with controlled embedding” by Andrea Corradini, Dominique Duval, Rachid Echahed, Frédéric Prost and Leila Ribeiro has been accepted for publication in Theoretical Computer Science.
• The paper “Purely Quantum Polar Codes” by Frédéric Dupuis, Ashutosh Goswami, Mehdi Mhalla and Valentin Savin has been accepted in QIP 2020.

October 2019:

• The paper “Proof Technology and Learning in Mathematics: Common Issues and Perspectives” by N. Balacheff and T. Boy de la Tour appeared in the Mathematics Education in the Digital Era book series (MEDE, volume 14).

September 2019:

• The paper ” Prenex Separation Logic with One Selector Field ” by M. Echenim, R. Iosif and N. Peltier was presented at TABLEAUX 2019.
• The paper: “Ilinva: Using Abduction to Generate Loop Invariants” by M. Echenim, N. Peltier and Y. Sellami was presented at FroCoS 2019.

June 2019:

• The paper “Communication through coherent control of quantum channels” by Alastair A. Abbott, Julian Wechs, Dominic Horsman, Mehdi Mhalla and Cyril Branciard has been accepted for presentation at AQIS 2019.
• The paper “Purely Quantum Polar Codes” by Frédéric Dupuis, Ashutosh Goswami, Mehdi Mhalla and Valentin Savin has been accepted for presentation at ITW 2019.
• The paper “Contextuality in multipartite pseudo-telepathy graph games ” by Anurag Anshu, Peter Hoyer, Mehdi Mhalla, Simon Perdrix has been accepted for publication in the Journal of Computer and System Sciences.

April 2019: The paper The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains (by M. Echenim, R. Iosif and N. Peltier) was presented at the 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).

February 2019: The paper The PBPO graph transformation approach (by A. Corradini, D. Duval, R. Echahed, F. Prost and L. Ribeiro) appeared in the Journal of Algebraic Methods in Programming.

Members

Scientific Leader

• Nicolas Peltier (CNRS Researcher, HdC)
  Office: 480, Phone: 04 57 42 15 40
  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: rachid.echahed@imag.fr
• Mehdi Mhalla (CNRS Researcher)
  Office: 484, Phone: 04 57 42 15 30
  Email: mnacho.echenim@imag.fr
• Rachid Echahed (CNRS Researcher, HdC)
  Office: 481, Phone: 04 57 42 14 90
  Email: mehdi.mhalla@imag.fr
• François Puitg (associate lecturer UGA)
  Office: 483, Phone: 04 57 42 15 46
  Email: francois.puitg@imag.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