About the position
Context
Project
The postdoc 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 and the remote supervision of
Enrico Tassi from the STAMP team in Sophia-Antipolis and
Matthieu Sozeau from the GALLINETTE team in Nantes. There will be regular meetings with co-supervisors either remotely or face to face, as well as occasional meetings with participants from the other work packages of the Liberabaci project.
Travel expenses are covered within the limits of the scale in force.
Assignment
Assignments
With the help of people from the projects and their collaborators, the recruited person will work on Rocq extensions and libraries in order to improve their usability. The user experience will be revised from scratch targetting the full range between beginner and expert users. It might be useful to conduct interviews with Rocq users to assess the actual requirements. It will then be necessary to design new domain specific languages, to make the tactic language and structure declaration mechanism of Rocq more flexible, easier to explore, but also more stable. The design and implementation of new algorithms in type theory might be required.
The expected outcome of this work are new interfaces to build libraries of formal content in Rocq, research publications in proceedings or journals, as well as oral presentations in workshops and conferences.
For a better knowledge of the proposed research subject
We suggest to read the following papers.
Matthieu Sozeau. A New Look at Generalized Rewriting in Type Theory.
Journal of Formalized Reasoning
, 2009, 2 (1), pp.41-62.
⟨inria-00628904⟩
Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi.
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction
, Jun 2020, Paris, France. pp.34:1--34:21,
⟨10.4230/LIPIcs.FSCD.2020.34⟩
.
⟨hal-02478907v6⟩
Davide Fissore, Enrico Tassi. A new Type-Class solver for Coq in Elpi.
The Coq Workshop 2023
, Jul 2023, Białystok, Poland.
⟨hal-04467855⟩
Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence.
ACM Transactions on Programming Languages and Systems (TOPLAS)
, 2025, pp.1-40.
⟨10.1145/3737283⟩
.
⟨hal-05192017⟩
Collaboration
The recruited person will be mainly in connection with Cyril Cohen, Enrico Tassi and Matthieu Sozeau, but will also work remotely with other members of the Liberabaci project or any appropriate collaborator that may help with their research.
Responsibilities
The person recruited is responsible for setting up the tools and methodology required to complete their assignment, with help from their supervisors and reaching out for external experts if required, especially in human computer interaction.
Main activities
Main activities:
Assess the needs and design languages and their interpretation accordingly
Setup the infrastructure
Implement extensions of Rocq.
Document the resulting software.
Collect user feedback
Write research papers and communicate towards peers.
Additional activities:
Design or integrate user interfaces to developement environments.
Anticipate a long term maintainance scheme for these.
Skills
Technical skills and level required
Know very well at least one proof assistant, preferably one based on dependent type theory.
Strong knowledge in Human Machine Interaction.
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.
This listing was collected from a public source and is reproduced here for
information only. Always confirm the details on the original posting before applying.
View the original posting