PhD in mathematics and fondamental computer science (M/F)

Job Description

Thesis Subject

Linear duality and higher algebraic effects in homotopy type theory

The goal of this PhD thesis will be to define a unified, syntactic, and functorial framework that integrates linear logic, algebraic effects, and homotopic type theory. To this end, we will start with the semantic interpretation of a system of dependent types with universe Type : Type as defined in the language of domain theory. The first step will be to axiomatize the structures of this semantic interpretation and to establish a connection with the relational model of linear logic. We will then formulate extensions of the theory of dependent types with intersection types, drawing on the correspondence between intersection types and finite elements of the relational semantics. In parallel, we will study the connections between linear continuations, duality in dialogue games, and higher algebraic effects, within the framework of a homotopic and multimodal type theory.

Skills:
- Good knowledge of the syntax and semantics of dependent type theory with equality
- Good knowledge of a proof assistant such as Agda, Isabelle, Lean or Rocq in terms of formalisation and implementation
- Good knowledge of one programming language such as Haskell, OCaml or Rust

- English: B2 (European Framework of Reference)
- Ability to conceptualise
- Critical thinking skills
- Organisational skills
- Ability to work in a team

Your Work Environment

The aim of the project is to participate in the development of a new generation of proof assistants that integrate both a linguistic layer and automated assistance tools to guide scientists and facilitate the construction of certified mathematical documents, from the choice of concepts and definitions to the elaboration of theorems and proofs.

Constraints and risks

None

Compensation and benefits

Compensation

2300 € gross monthly

Annual leave and RTT

44 jours

Remote Working practice and compensation

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

About the offer

About the CNRS

The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.

CNRS

The research professions