PhD Position F/M Theory and Implementation of Universal Algebra

Context

Project
The relai-thèse will take place within the framework of the défi Inria Liberabci
, which objectives are to make complex tools such as Hierarchy Builder, Trocq or rewriting, as well as libraries of formalized mathematics such as mathematical components accessible to users that are not specialized in formal proofs (e.g. undergraduate students, math/CS teachers or other peers) via the development of convenient interfaces, needing theoretical adjustments.
Location
The research will be carried out in the LIP laboratory of ENS Lyon under the local supervision of Cyril Cohen
, within the CASH team.
Travel expenses are covered within the limits of the scale in force.

Assignment

Assignments
Mathematical objects are often organized in a hierarchical setting. A new theory can often be framed as a generalization or, dually, as a specialization of another one, possibly not in a unique way. A full specification of this taxonomy is, of course, left implicit in mathematical writing, since the author can rely on the reader’s expertise to reconstruct its relevant parts for the argument at hand. In the setting of formalized mathematics through the use of proof assistants and interactive theorem proving, such implicitness is not possible, and a need arises for specification and retrieval of these connections. More specifically, users must be able to introduce and relate abstract theories, extend them with new constructions, and prove relevant theorems. Furthermore, they need the capability to instantiate these theories with concrete models and specialize previously established results. In this work we tackle these challenges from various perspectives. First, in the setting of univalent foundations, we present a development specific to algebraic structures: the Universal Algebra library for UniMath. Second, we describe and present an operational semantics for Hierarchy Builder , a high-level tool for specifying mathematical hierarchies in Roc and conveniently applying results from abstract theories to their models. Lastly, we investigate the relationship between scoped and unscoped syntaxes both from the perspective of Categories with Families and from an implementation perspective.

Main activities

Figure out theoretical aspect of algebraic structures
Write code in Rocq, elpi and possibly Caml
Submit research papers
Present research activities to peers and students.

Skills

Technical skills and level required
Know very well at least one proof assistant, preferably one based on dependent type theory.
Know metaprogramming for proof assistants.
Languages
Advanced English.
Relational skills
Communicate about your ideas and results.
Work autonomously, while talking about strategic decisions with other members of the project.
Listen to feedback.
Other valued appreciated
Expertise in Rocq.
Knowledge of Rocq-ELPI and Hierarchy Builder
Git, GitHub, and other common software development tools.