Post-Doctoral Research Visit F/M User Experience for formal proofs in practice

Improve the usability of Rocq extensions and formal-proof libraries for beginners through expert users. The project may involve user studies, new domain-specific languages, more flexible tactic and structure mechanisms, and algorithms in type theory. Work with the Liberabaci collaborators on interfaces, implementations and publications. The 12-month Lyon appointment starts 1 February 2027; gross monthly pay is EUR 2,788.

A PhD or equivalent; strong knowledge of a proof assistant, preferably based on dependent type theory, and human-computer interaction. Advanced English; Rocq, Rocq-ELPI, Hierarchy Builder and collaborative development tools are useful. Restricted-area security authorisation may be required.