PhD in Foundational Computer Science: Linear Duality and Higher Algebraic Effects in Homotopy Type Theory

This PhD position at the Institut de Recherche en Informatique Fondamentale (Paris) focuses on developing a unified syntactic and functorial framework integrating linear logic, algebraic effects, and homotopy type theory. The project aims to formalize and implement these concepts in proof assistants like Agda, Lean, or Isabelle, advancing the next generation of certified mathematical assistants. The work will bridge theoretical foundations with practical applications in automated proof guidance and certified document construction. Applicants should have a strong background in dependent type theory and formal verification tools, with proficiency in functional programming languages. The position offers a collaborative environment within a leading French research institution.

• Develop a unified syntactic and functorial framework for integrating linear logic, algebraic effects, and homotopy type theory.
• Axiomatize and formalize the semantic interpretation of dependent type systems with universes in domain theory.
• Investigate the relationship between intersection types and finite elements in relational semantics.
• Study connections between linear continuations, dialogue duality, and higher algebraic effects in multimodal homotopy type theory.
• Implement and test the proposed theories in proof assistants (Agda, Lean, Isabelle, or Coq).
• Collaborate with the team to design tools for automated proof guidance and certified document construction.
• Publish research findings in peer-reviewed conferences and journals.