I am an Assistant Professor (Maître de conférences) at the Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE) and a permanent member of the formal methods team Méthodes, at Samovar laboratory (Télécom SudParis), part of Institut Polytechnique de Paris. I am also an associate member of the LDBC SNB organization. Currently, I am working on the certification of data-centric languages, algorithms, and static program analyzers, using Coq/SSReflect, as well as on graph database topics.

• I participate in the following outreach initiatives : SIGPLAN-M (Long-Term Mentor), Declics (Popularising CS topics to high-school students), Gender Parity in Academia (CGE Working Group).
• Together with Evelyne Contejean, I coordinate the TransForm working group (Labex DigiCosme).
• In 2021, I'm in the PC of the events below. Previous service: here.
  EDBT Regular & Short Papers Tracks (CfP), SIGMOD Demo Track (CfP), MEDI (CfP), POPL Artifact Evaluation Track (CfP), PLDI Artifact Evaluation Track (CfP), PxTP-7 (CfP - Deadline: 21/04), SBLP (CfP - Deadline: 09/05), GRADES-NDA (CfP - soon). Consider submitting!
• The vision article on the future of graph processing systems, written together with fellow Dagstuhl Seminar 19491 participants, got accepted to the Communications of the ACM Journal! You can read it here
• [09/06/20] Invited seminar at the IMDEA Institute on the mechanically verified VerDILog graph query engine
• [16-18/12/19] Presentation of the GRASP tool for approximate querying on graph summaries at SUM.
• [01-06/12/19] Invited participant at the Dagstuhl Seminar 19491 on "Big Graph Processing Systems".

Research Topics

• formalization of high-level languages and declarative programming
• certification of inference engines for relational, deductive, and graph databases
• proof assistants (Coq, Isabelle) and logical frameworks (Twelf/LF, MMT)
• computer-aided formal verification of mathematics
• foundations of mathematics (logic, category theory, type theory)

• Graph Summarization (to appear),
  with A.Bonifati, H.Kondylakis
  Encyclopedia of Big Data Technologies'20

• The Future is Big Graphs! A Community View on Graph Processing Systems (to appear),
  with S.Sakr, A.Bonifati, A.Iosup, H.Voigt, and participants of the Dagstuhl Seminar 19491,
  Communications of the ACM'21


• Graph Queries: From Theory to Practice ,
  with A.Bonifati, ACM Sigmod Record'18, vol. 47, Nº 4: 5-16.
  DB Principles Column (Invited Paper)


• Certified Graph View Maintenance with Regular Datalog ,
  with A.Bonifati and E.J.Gallego Arias,
  Theory and Practice of Logic Programming Journal, TPLP'18, vol. 18, Nº 3-4: 372-389;
  presented at the 34th International Conference on Logic Programming, ICLP@FLoC'18, Oxford, UK. VerDILog Code

• Approximate Querying on Property Graphs,
  with A.Bonifati, A. Nazabal and R. Vuillemot,
  Scalable Uncertainty Management, SUM'19, Compiègne, France.


• Certifying Standard and Stratified Datalog Inference Engines in SSReflect,
  with V.Benzaken and E.Contejean,
  Interactive Theorem Proving, ITP'17, Brasilia, Brazil: 171 - 188, LNCS 10499.
  DatalogCert Code


• A Coq Formalization of the Relational Data Model ,
  with V.Benzaken and E.Contejean,
  European Symposium on Programming, ESOP'14, Grenoble, France: 189 - 208, LNCS 8410.

• A Case Study on Formalizing Algebra in a Module System ,
  with F.Horozal and K.Sojakova,
  Modules and Libraries for Proof Assistants, MLPA'09, Montreal, Canada: 11 - 18, ACM 429.

• Une formalisation en Coq du modèle relationnel de données ,
  with V.Benzaken and E.Contejean,
  Actes des Septièmes Journées Nationales GDR-GPL'15, Bordeaux, France: 83 - 86.

• Approximate Evaluation of Label-Constrained Reachability Queries,
  with A.Bonifati, A. Nazabal Ruiz-Diaz, and R.Vuillemont.
  

• A Coq Formalization of Relational and Deductive Databases - and Mechanization of Datalog,
  PhD Thesis, Université Paris-Sud, Defended: 02/12/2016


• A Type Theory with Reflection,
  MSc Thesis, Jacobs University Bremen, 2012


• Structured Specification with Hiding in the Edinburgh Logical Framework LF,
  BSc Thesis, Jacobs University Bremen, 2010

Supervision

• Master Level Research Internships


• Université Claude Bernard Lyon 1, 03-09/2018, Database Team, LIRIS Research Laboratory
  Amaia Nazábal Ruiz Díaz - now: Full Stack Developer, Gistia, Paraguay
  Approximate Query Processing on Property Graph Summaries


• ENSIIE, 06-08/2020, co-supervision with Ane-Laure Ligozat (DD&RS ENSIIE)
  Eva Bilski - EcoMap - Building Sustainable Development City Maps with the Neo4j Graph Database

Teaching

• MdC, ENSIIE, since 09/2019:


• [TD/TP] Bases de Données - taught by M. Szafranski - Level: S1


• [18/10/2019] (legacy slides) Database Normalization .
• [25/10/2019] (only in 2019-2020) Recursive Query Processing .
• [13/12/2019] (extended as part of the GDA module) Introduction to Graph Databases.
• [TP] Programmation Impérative (IPI) - taught by G. Burel - Level: L3


• [TD/TP] Langages Formels, Validation et Vérification du Logiciel (VVL) - taught by C. Dubois - Level: M1


• [Coordinator/Responsable de l'UE] Gestion de Données Avancée (GDA) - Level: M1


• Advanced SQL (module 1) - taught by P. Poucheral
• [Coordinator/Responsable de cours] Semi-structured Data Models (RDF & PGM) (module 2)
• [UE] Programmation Fonctionnelle (IPF) - Level: L3


• [ Coordinator/Responsable de cours] Introduction à la programmation fonctionnelle (module 1)
• [TD/TP] Logique (module 2) - taught by J. Forest - Level: L3
• [TP] (only in 2019-2020) Programmation Web (IPW) - Level: L3
• Vacataire, Université Rennes 1, 2018-2019: 40h
• [TP Scala] Initiation au Génie Logiciel - Level: S4, 40h
• Vacataire, Université Claude Bernard Lyon 1, 2016-2018: 71h
• [ TD] Bases de Données Déductives - Level: M1, 10h
• [ TP Java & DES - Datalog Educational System ] Bases de Données Déductives - Level: M1, 20h
• [ TD ] Programmation Fonctionnelle pour le Web - Level: S4, 3h
• [ TP JavaScript ] Programmation Fonctionnelle pour le Web- Level: S4, 18h
• [ TD ] Algorithmique Numérique - Level: S6, 20h
• ATER, Université Paris-Saclay, 2015-2016: 95h
• [TP C/C++] Mathématique pour l'informatique 1 - Level: S3, 20h
• [ TP C/C++] Mathématique pour l'informatique 2 - Level: S4, 20h
• [ TP OCaml] Introduction à la programmation fonctionnelle - Level: S4, 16h
• [TP OCaml] Projet de programmation fonctionnelle avancée - Level: S6, 39h
• Monitrice, IUT d'Orsay, 2014-2015: 64h
• [TP Java/Oracle SQL] Bases de données avancées - Level: S3, 32.5h
• [TD] Programmation et administration des bases de données - Level: S2, 21h
• [TP Oracle SQL] Programmation et administration des bases de données - Level: S2, 10.5h
• Monitrice, IUT d'Orsay, 2013-2014: 64h
• [TD] Programmation et administration des bases de données - Level: S2, 42h
• [TP Oracle SQL] Programmation et administration des bases de données - Level: S2, 22h
• Teaching Assistant, Jacobs University Bremen
• [TD (in English)] Mathematics Support Center - Level: S1-S6
• [TD (in English)] General Mathematics and Computational Science 1 - Level: S1
• [ TD (in English)] General Mathematics and Computational Science 2 - Level: S2

Activities

• PC Member:
• 2021
• EDBT International Conference - Regular Research Papers Track
• MEDI International Conference - Regular Research Papers Track
• PxTP International Workshop on Proof eXchange for Theorem Proving
• BSPL Brasilian Symposium on Programming Languages
• SIGMOD International Conference - Demo Track
• POPL International Conference - Artifact Evaluation Track
• PLDI International Conference - Artifact Evaluation Track
• 2020
• EDBT International Conference - Regular & Short Research Papers Tracks
• The Coq Workshop
• POPL International Conference - Artifact Evaluation Track
• Subreviewer: IJCAR 2020, TYPES 2019 , PODS 2019 , VLDB 2019 , VLDB 2018 , PODS 2017 , VLDB 2017


• Journal Review:
  
  • International Journal on Very Large Databases (VLDB 2021)
  • ACM Transactions on Database Systems (TODS 2020)
  • Information Systems Special Issue (AMW 2019)
• Administrative Duties:
• Responsible for the Advanced Databases (GDA) & Blockchain (BLK) courses at ENSIIE
• Elected member of the LRI laboratory council: 2014-2015
• Elected representative of the EDIPS Computer Science PhD Students: 2012-2014
• Student Member of the Organizing Committee: CICM 2012 , NWERC 2010 , ESSLLI 2009

Bio

• 2018 - 2019
  I was a postdoctoral researcher in the INRIA team Celtique, at the IRISA laboratory, working with David Pichardie, in the context of his ERC Consolidator "Verified Static Analysis Platform" project.


• 2017 - 2018
  I was a postdoctoral researcher at Université Lyon 1, where I collaborated with Angela Bonifati, in the context of the ANR DataCert project.


• 2012 - 2016
  I earned a PhD in Computer Science, at Université Paris-Sud, in the VALS team, at the LRI research laboratory, supervised by Véronique Benzaken and Evelyne Contejean.


• 2007 - 2012
  I studied at Jacobs University, where I obtained a BSc in Mathematics and a MSc in Computer Science. I was part of the KWARC team, working in the LATIN project, supervised by Florian Rabe and Michael Kohlhase .


• I grew up and was born in Iasi, Romania.

Talks

• 09/06/2020, Mechanically Verified Graph Query Processing ,
  IMDEA Software Institute , Madrid, Spain


• 17/12/2019, Approximate Querying on Property Graphs ,
  SUM International Conference , Compiègne, France


• 02/12/2019, Graph Query Processing Techniques ,
  Dagstuhl Seminar: Big Graph Processing Systems , Dagstuhl, Germany


• 23/02/2019, Certified Graph Query Processing ,
  EUTypes Workshop @ Lambda Days , Krakow, Poland


• 31/01/2019, Foundational Approaches to Graph Query Processing ,
  LIMOS Seminar , University of Auvergne, Clermont-Ferrand, France


• 15/07/2018, Certified Graph View Maintenance with Regular Datalog ,
  34th International Conference on Logic Programming (ICLP) @ Federated Logic Conference (FLoC), University of Oxford, Oxford, United Kingdom


• 18/06/2018, Certified Graph View Maintenance with Regular Datalog ,
  Plume Seminar , Ecole Normale Supérieure Lyon, Lyon, France


• 14/11/2017, Certifying Deductive Database Engines with Coq/SSReflect ,
  LFCS Seminar , University of Edinburgh, Edinburgh, United Kingdom


• 26/09/2017, Certifying Standard and Stratified Datalog Inference Engines in SSReflect ,
  8th International Conference on Interactive Theorem Proving (ITP) , University of Brasilia, Brasilia, Brazil


• 02/07/2014, Toward Data Intensive System Certification ,
  DigiCosme Paris-Saclay Research Day , Orsay, France


• 22/01/2013, Certifying Data-Centric Languages and Systems ,
  Programming Languages Mentoring Workshop (PLMW) @ Symposium on Principles of Programming Languages (POPL), Rome, Italy


• 01/07/2010, Structuring Theories with Partial Morphisms ,
  20th International Workshop on Algebraic Development Techniques (WADT), Schloss Etelsen, Germany

Software

• GRASP (with A.Bonifati, A.Nazabal, R.Vuillemont) :
  approximate evaluation of count queries on summaries of property graphs
• VerDILog (with A.Bonifati and E.J.Gallego-Arias) :
  certified, incremental graph view evaluation & maintenance for regular Datalog
• DatalogCert (PhD supervisors: V.Benzaken and E.Contejean) :
  certified evaluation engines for standard and stratified Datalog

Resources

• Datalog Educational System
• Neo4j Desktop
• Graph Algorithms - Practical Examples in Apache Spark & Neo4j
• Graph Databases