UMR8243-OMUAVC-007 - PhD Student (M/F) at IRIF - formalization of commutative diagram proofs
General information
Offer title : Offer title : PhD Student (M/F) at IRIF - formalization of commutative diagram proofs (H/F)
- Reference : UMR8243-OMUAVC-007
- Number of position : 1
- Workplace : PARIS 13
- Date of publication : 23 August 2024
- Type of Contract : PhD Student contract / Thesis offer
- Contract Period : 36 months
- Start date of the thesis : 1 December 2024
- Proportion of work : Full time
- Remuneration : 2 135,00 € gross monthly
- Section(s) CN : Information sciences: bases of information technology, calculations, algorithms, representations, uses
Description of the thesis topic
Context of the PhD work
The recent advent of applied category theory (ACT) and large-scale projects to formalize mathematics using proof assistants such as Coq, Isabelle/HOL, or Lean have opened up promising research avenues at the crossroads of several theoretical disciplines. We propose to combine these paradigms in a field of research in theoretical computer science that lends itself ideally to it: the theory of compositional categorical rewriting, a modern generalization of the algebraic approach to graph rewriting.
Starting from the pioneering work of Ehrig et al. in the early 1970s, with as a critical milestone the introduction of the theory of adhesive categories introduced by Lack and Sobocinski in the early 2000s, the categorical rewriting approach allows to deal with a wide variety of systems of practical and theoretical interest and has de facto imposed itself as the standard approach in the field. A peculiarity of categorical rewriting lies in the nature of lemmata and proofs in this formalism, which makes intensive use of commutative diagrams and diagrammatic calculus. This naturally motivates the development of an appropriate approach to exploit this highly modularized mathematical reasoning within formal developments in Coq and explore the possibility of interacting with Coq in diagrammatic form. One of the main goals of this project is to develop and maintain an interactive Coq-based wiki system for categorical rewriting theory, aimed atboth certifying and preserving knowledge in this area of research in a modern and freely accessible format.
PhD Project Description
The project has several main objectives: developing a “reasoning move” framework for diagrammatic proofs within category theory, implementing this calculus in the proof assistant Coq, and developing a library of diagrammatic proofs for compositional rewriting theory. The starting point for this research will be recent advances achieved by the CoREACT team on conditional and generalized sketch calculi. The theoretical objectives of the PhD project are focused on exploring the “reasoning move” methodology within the context of category theory, including 1-category theory, double category theory, fibrational concepts, and, ultimately, categorical rewriting theory. This exploration will deepen the theoretical understanding of diagrammatic proofs within these areas.
The second objective is practically implementing the “reasoning move” calculus within the proof assistant Coq. This involves developing an efficient representation of the calculus in Coq and creating a comprehensive library of diagrammatic proofs tailored for compositional rewriting theory. The goal is to facilitate automated reasoning and proof verification, enhancing the usability of diagrammatic proof methods in formal verification processes. The development will build upon the diagrammatic editor YADE, which has some prototypical Coq mechanisation features for category theory (cf. https://hal.science/hal-04407118v1).
Overall, this project aims to advance the theoretical and practical aspects of diagrammatic proof calculi, providing valuable tools and insights for researchers and practitioners in formal methods and category theory.
Work Context
The ANR CoREACT project (2023-2027) is a national research project between Université Paris Cité (IRIF), École Polytechnique (LIX), ENS Lyon (LIP), and INRIA Sophia-Antipolis (cf. https://coreact.wiki/ for a complete list of consortium members). The project is organized in a highly collaborative fashion, with active interchanges between all consortium teams and regular online and in-person meetings. The PhD position will be co-supervised by Nicolas Behr (CNRS and Université Paris Cité, IRIF) and Ambroise Lafont (LIX, PARTOUT), with the primary host institution being IRIF. The project will be equipped with funding for attending national and international conferences, in addition to PhD training activities provided via the École Doctorale 386 (Université Paris Cité).
IRIF (PPS): The team Proofs, Programs and Systems of IRIF brings together researchers and students with various scientific backgrounds (in computer science and mathematics) to work on the theme of the foundations and practice of programming languages and distributed systems. PPS also develops methods and tools for modeling biological systems and new methods for developing and maintaining systems in a free software setting. Last, PPS is a major actor in the realm of proof assistants. PPS additionally runs the joint project PiCube with INRIA and plays a crucial role, in collaboration with INRIA and UPMC.
LIX (PARTOUT):Â The PARTOUT team explores deductive and computational formalisms, focusing on trustworthy and verifiable meta-theory. The team investigates the combinatorial and complexity-theoretic properties of these formalisms, and the essential nature of these formalisms, such as proof identity, which asks when two proofs of the same theorem are identical. This basic question remains unanswered in proof theory. Additionally, PARTOUT examines foundational meta-theory questions of logical and type systems, including cut-elimination, focusing, type soundness,and normalization theorems. This research emphasizes the relationships between computation and deduction, extending beyond the Curry-Howard correspondence. In particular, a key methodology consists of interpreting computation as deduction and vice versa, leading to both theoretical and practical research questions.