PhD positions

Dwarf galaxies are by far the most numerous galaxies in the Universe, but probably also the most difficult to find and characterise. Indeed, their small size and low surface brightness make them particularly difficult to detect outside our Local Group. However, two instruments are about to overcome these difficulties. The Euclid space mission is already a game changer. Thanks to its large field of view and excellent image quality, it can clearly identify large populations of dwarf galaxies, as well as their nucleii and globular cluster populations. At the same time, the ground-based LSST experiment with the Rubin telescope will collect complementary data, in particular detailed colour information. The combination of LSST and Euclid photometry will, for example, help to rule out background galaxies as dwarf candidates and make it easier to identify the population of globular clusters (GCs). 

The PhD student will have privileged access to both sets of data at a critical time, thanks to the PhD supervisor's tickets. The long term aim of the thesis, which will be carried out in close collaboration with the international Euclid and LSST consortia, will be to:

- Identify the population of dwarf galaxies in a specific region of the sky - that around the Fornax supercluster. This region has been chosen because its density minimises the risk of contamination by background objects and maximises the chances of finding globular-cluster-rich objects, for which numerous follow-up studies may be done. 

- study the spatial distribution of dwarfs relative to the most massive galaxies, and the implications for nucleus and globular cluster content. Due to a lack of statistics, the causes of the large variations in the GC content of the dwarf population are still largely unknown. 

- Determine the most relevant parameters to fully characterise the dwarf populations (e.g. effective radius, surface brightness, colour, dark matter content), providing insightful criteria for their identification in the remaining Euclid and LSST surveys. 

One of the big challenges of this work is the large set of data currently available. The analysis of this data set require the development of ad hoc artificial intelligence tools. They are needed to : 

- detect and segment the LSB candidates in the images 

- validate their status as dwarf dwarf galaxies, excluding background objects with the caveat that their distances are not known 

- Determine automatically their properties 

Two ways have so far been explored : 

- Using pre-trained foundation models (I.e. galaxy Zoo) on image cutouts (when catalogs of sources are available), and further eye validation (with costumed visualisation tools) 

- Using dedicated neuronal networks and ad hoc filters (i.e. Gabor filters) to directly detect/segment the candidates, taking into account foreground or background contaminants (e.g. Galaxy cirrus) without the need of pre-defined cutouts 

Both methods will be compared, and their effectiveness depending on image depth, and availability of multi-sectral information will be analysed.

The strong gravity of a massive black hole disturbs stars up to break up point. The project follows a theoretical approach for the integration of stellar orbits in general relativity applied to a realistic population of stars in the core of a galaxy. A key objective is to map these high energy events to high accuracy with a view to apply machine learning methods to probe real galaxies as observed by e.g. the James Webb Space Telescope (JWST). To reach that goal, this project aims to quantify the growth rate of black holes in order to explain their very existence in the early Universe (< 1 Gyr), a key challenge of modern astrophysics.

A blockchain is a distributed ledger maintained by a peer-to-peer network, where the nodes apply a consensus algorithm to agree on the recording of new data. Three properties define these systems: efficiency (transaction throughput), decentralization (distribution of control across nodes), and security (resistance to adversarial attacks). The original consensus mechanism, Proof of Work (PoW), relies on computational competition among nodes to solve cryptographic puzzles—a process that incurs substantial energy costs. This PhD project focuses on Proof of Stake (PoS), the consensus protocol underpinning Ethereum and other next-generation blockchains. Unlike PoW, PoS selects validators probabilistically, with selection probabilities scaled by their staked cryptocurrency holdings. The chosen validator proposes the next block and earns a reward in return. While this design might intuitively favor wealthier participants, empirical and theoretical analyses reveal a counterintuitive property: the long-term stake distribution converges to a stable equilibrium on average—a phenomenon mathematically captured by Pólya urn models, a class of reinforced stochastic processes. Modern variants of Proof of Stake (such as Algorand or Ouroboros) lack a unified mathematical description. The objective is to develop a general framework to model these algorithms, drawing on the theory of reinforced stochastic processes and multi-color (or even infinitely many-color) Pólya urns to represent the large number of participants. 

The goal is to study their limiting behaviors and fluctuations to identify conditions that ensure fair decentralization. The work will also extend current theoretical results to better account for the heterogeneous and dynamic structure of blockchains (temporal variations in activity or transactional preferences). The second research axis adopts a queueing-theoretic framework to quantify blockchain transactional efficiency. Here, pending transactions are modeled as customers in a G/G/1 queue, where blocks act as batch-service events. We will analyze the arrival-process dynamics (e.g., transaction submission rates) and service discipline (block propagation and validation delays) to derive key performance metrics, including Mean confirmation time (time-to-inclusion in a block) and System congestion (mempool size evolution). Our approach begins with tractable M/M/1 and M/D/1 models (exponential/inter-determined arrivals and service times) to establish baseline results, then extends to non-Markovian settings (e.g., heavy-tailed distributions for bursty traffic). This progression will yield closed-form approximations for waiting-time distributions and throughputs. To bridge the gap between theory and practice, the model will integrate Two features. Fee-based prioritization as transactions compete for block inclusion via dynamic gas markets (Ethereum) or fee-per-byte auctions (Bitcoin). Time-sensitive abandonment as nodes may discard transactions with suboptimal fees after exceeding empirically observed patience thresholds (e.g., 95th-percentile waiting times). 

This project has two main objectives: 
- A rigorous mathematical characterization of Proof-of-Stake mechanisms, focusing on decentralization properties through stochastic reinforcement models. 
- A quantitative framework for blockchain efficiency, grounded in queueing theory to analyze transactional dynamics. 
By combining probabilistic modeling with empirical validation, the work will deliver both theoretical insights and practical metrics—essential for designing next-generation blockchains that balance fairness, scalability, and sustainability.

The cosmological model based on the existence of cold dark matter describes the large-scale structure of the Universe with great success, but it faces several challenges at the galactic scale. In particular, dark- matter-only simulations predict density profiles that are particularly steep at the center of dark matter halos — known as "cusps" — while some observations favor "cores" of constant density at the center. Introducing processes such as star formation and feedback phenomena resulting from stellar evolution and active galactic nuclei (which include stellar winds, radiation effects, supernova explosions, and jets) into simulations can alleviate this tension by reproducing cores. However, simulations agree neither on the intensity of these processes nor on their effect on dark matter distribution. Furthermore, observations indicate a diversity of dark matter density profiles for a given total mass, contrary to expectations if these processes were the same from one galaxy to another. Finally, some observations seem to indicate the presence of dark matter cores early in the history of the Universe, which requires halo transformation mechanisms that are sufficiently rapid. These challenges raise fundamental questions about the formation mechanisms of dark matter cores, feedback phenomena, and more generally, the very nature of dark matter. The methods used to infer dark matter density profiles from galaxy kinematics rely on various physical assumptions, particularly regarding the equilibrium of galaxies, their axisymmetry, and the ratio between circular motion and velocity dispersion. They also rely on Markov Chain Monte Carlo (MCMC) methods, which prove to be too costly in terms of time and computing capacity when studying samples of more than a dozen galaxies. Indeed, the data used are three-dimensional multispectral cubes (two spatial dimensions, one velocity dimension; the pixels are spectra whose components are Doppler-shifted due to gas movements) which are particularly voluminous, and the models used require dozens of parameters per galaxy. Yet, future great observatories such as the Square Kilometre Array (SKA), the Extremely Large Telescope (ELT), as well as new instrumentation for the Very Large Telescope (VLT), will soon produce unprecedented amounts of data from which it will, in principle, be possible to deduce dark matter density profiles and their evolution over a large part of the history of the Universe. 

The aim of this thesis is, on one hand, to test the physical assumptions of the methods used to deduce dark matter density profiles using simulations of isolated galaxies (produced as part of the thesis) and existing cosmological simulations; and on the other hand, to optimize these methods so they can be applied to future observational surveys. Several directions are envisioned in this regard: porting existing methods to GPUs, accelerating Monte Carlo methods by optimally sampling the probability distribution, and exploring new methods such as Bayesian neural networks. 

This thesis will be carried out within the framework of the IRMIA++ Interdisciplinary Thematic Institute, which brings together mathematicians, computer scientists, and astrophysicists. It will notably benefit from a collaboration within the IRMA statistics team with Augustin Chevallier.

Homotopy Type Theory (HoTT) is a contemporary approach to the foundations of mathematics that draws on ideas from logic, theoretical computer science, and homotopy theory. HoTT is built on type theory, which already serves as the foundation for proof assistants such as Lean and Rocq, and introduces a radical change: instead of considering the fundamental objects of the theory to be sets, HoTT uses spaces (infinity-groupoids). The entire language thus takes on a topological character: proofs of equalities become paths, statements are automatically homotopy-invariant, and so on. This shift in perspective is doubly useful: 
- For the computer scientist, it fills some gaps in Martin-Löf type theory by introducing quotient types, function extensionality, and the ability to do representation-independent reasoning. 
- For the mathematician, it provides a framework for developing homotopy theory in a synthetic and constructive manner, without having to rely on combinatorial models such as simplicial sets. 
In technical terms, HoTT adds two axioms to the language of type theory: the univalence axiom, which identifies equality between types with equivalences, and higher inductive types (HITs), which allow for the definition of higher dimensional types [5]. However, HoTT leaves out an important aspect of the theory: its effectiveness. Indeed, the language of type theory has a well-defined computational behavior, which lets us evaluate any proof of a concrete statement and obtain an explicit value. But the axioms added by HoTT have no clear computational content. Today, the only way to evaluate a proof written in HoTT is through cubical type theory (CTT) [3], which is a different extension of type theory that implements the HoTT axioms while retaining computational content. However, in practice, it is not always easy to compute with CTT! 

The goal of this thesis is to study how to compute efficiently with HoTT and CTT. We propose three approaches: 

I. Computing topological invariants with CW complexes Thanks to its effectiveness, it is theoretically possible to use CTT to compute topological invariants such as homotopy groups and (co)homology groups based on their mere definitions (provided they are constructive). However, a naive definition will not yield an efficient computational algorithm: a well known example is the Brunerie number [1], an integer defined in CTT via homotopic constructions which we know mathematically should evaluate to -2, but its evaluation fills up the computer's memory. We propose to investigate more suitable definitions for computation, such as the definition of homology groups of CW complexes [4] in terms of cellular homology and matrix operations. 

II. Evaluating Cubical Type Theory using Rocq In addition to the use of overly naive definitions, one reason for the inefficiency of CTT is that the only available implementation, Cubical Agda, is not optimized for computation. In contrast, Rocq and Lean offer powerful tools for evaluating definitions by compiling them down to native code. We propose to define a syntactic translation from CTT to Rocq's type theory, based on the method outlined in [2]. This will, on the one hand, provide the first fully formal framework for studying the semantics of CTT, and on the other hand, allow us to leverage Rocq's capabilities to evaluate definitions in CTT. 

III. Conservativity of Cubical Type Theory CTT is currently the only available tool for evaluating proofs written in HoTT. However, since CTT's language is richer than that of HoTT, there is a priori no guarantee that a result obtained by computation in CTT corresponds to an equality which is provable in HoTT. Conservativity results exist for integers, but the problem remains wide open for more complex types. We propose the use of syntactic methods (as in Part II) to address this problem. In the longer run, we could envision an automated tool that takes a proof in CTT and reconstructs a proof of the same statement in HoTT. 

[1] Guillaume Brunerie. Sur les groupes d'homotopie des sphères en théorie des types homotopiques. PhD thesis, Université Nice Sophia Antipolis, 2016.
[2] Loïc Pujet. Computing with Extensionality Principles in Type Theory. PhD thesis, Université de Nantes, 2022. 
[3] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. 2017.
[4] Axel Ljungström and Loïc Pujet. Cellular methods in homotopy type theory, 2026. submitted. 
[5] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013.