## Research Themes

### Coinductive proof search** **

Proof search is a paradigmatic computational process in logic with applications in automated reasoning and logic programming. CMAT researchers and collaborators are developing an original and fruitful approach to the area based on typed lambda-calculi.

Supervisors and contacts: José Espírito Santo (UM|CMAT) and Luís Pinto (UM|CMAT)

jes@math.uminho.pt; luis@math.uminho.pt

### Contributions to species distribution modelling of spatial big data** **

The ongoing climate changes and the need to improve knowledge about their impact on biodiversity call for the analysis of spatially extensive data on species communities to understand and forecast distributional changes of the underlying stochastic processes. The research program aims to investigate the problem of dealing with numerous species efficiently, while explicitly accounting for spatial structure in the data. The current applications are generally limited to relatively small spatial datasets due to computational burden problems that arise as the number of spatial locations increases. It becomes urgent to consider statistical methods able to overcome the usual scability constraints associated to joint species modelling over large regions. The theoretical methods to be investigated will be strongly motivated.

Supervisors and contacts: Raquel Menezes (UM | CMAT) and Isabel Natário (UNL | CMA-FCT)

### Curry-Howard isomorphism for the sequent calculus

A question in the areas of proof theory and lambda-calculus is: given that the theory of combinators corresponds to Hilbert systems, and the lambda-calculus corresponds to natural deduction, what version of the lambda-calculus does correspond to the sequent calculus?

Supervisors and contacts: José Espírito Santo (UM|CMAT) and Luís Pinto (UM|CMAT)

jes@math.uminho.pt; luis@math.uminho.pt

### Developing Novel Techniques for Gait Dynamics Analysis Using Topological Data Analysis and Neural Networks** **

This project aims to develop and test new mathematical and statistical techniques for analyzing complex time series data, specifically for assessing human gait dynamics. The goal is to find new insights into individual gait dynamics and classification, as well as to improve the interpretability and performance of neural networks used in the learning process. The project will utilize topological data analysis to optimize the performance of data-driven machine learning models and will be evaluated with existing and newly collected gait time series for predicting and monitoring neurological diseases of individual patients.

Supervisors and contacts: Flora Ferreira (UM | CMAT) and Wolfram Erlhagen (UM | CMAT)

fjferreira@math.uminho.pt; wolfram.erlhagen@math.uminho.pt

### Differential Equations: theory, modelling and applications

Ordinary and Partial Differential Equations (ODEs and PDEs) are of great relevance when one pretends to describe natural or physical phenomena using a universal and accurate language such as mathematics.

Within this range of mathematical theory, modelling and applications, several problems can be addressed in a Ph.D. project, according to the student’s profile and interests.

Supervisors and contacts: Eurica Henriques (UTAD|CMAT) and Ana Jacinta Soares (UM|CMAT)

eurica@utad.pt; ajsoares@math.uminho.pt

### Distributed statistical learning

Statistical learning methods facilitate pattern and relationship discovery within datasets and offer insight based on these patterns. Present approaches rely heavily on data collection and processing at a central location. This centralization makes the system brittle, posing the risk of a single point of failure during computation. It neglects the possibility of harnessing edge computing, both in the devices and the network edge, and can add data privacy concerns when integrating federated data across different ownership domains.

To address these concerns, this research aims to develop novel distributed algorithms and implementations for statistical learning. These methods can overcome the constraints of centralized resources, avoid single points of failure, and address naturally distributed data, such as sensor networks. Additionally, this work intends to also account for time-evolving data.

Supervisors and contacts: Raquel Menezes (UM | CMAT) and Carlos Baquero (FEUP-UP | INESC)

rmenezes@math.uminho.pt

### Dynamics of Holder maps

Smooth dynamical systems are nowadays a quite well establish theory whereof its stability and genericity are very well studied. We intend to pursued towards weaker topologies namely what kind of results still prevails under Holder regularity?

Supervisors and contacts: Davide Azevedo (UM | CMAT) and Mário Bessa (UAB | CMUP)

davidemsa@math.uminho.pt

### Geometric symmetries via algebraic and computational tools

It is possible to approach the study of geometric objects admitting abundant symmetries via algebraic, and indeed, algorithmic procedures. Homogeneous manifolds form the central examples of this approach, and provide a fertile ground for studying the interplay between geometric and algebraic structures. We propose to study these hands-on spaces under the influence of a (pseudo-)Riemannian metric, aided by software such as Maple and LiE to implement symbolic and numerical methods to explore and deepen our understanding of this fundamental mathematical framework in differential geometry.

Supervisors and contacts: Ana Cristina Ferreira (UM|CMAT) and Henrik Winther (UiT-Norway)

anaferreira@math.uminho.pt

### Impact of parameter estimation in state space models associated to the Kalman filter

The Kalman filter is a widely used tool for state estimation in state space models. However, the accuracy of the state estimation strongly depends on the quality of the model parameter estimation. Uncertainty and imprecision in parameter estimation can lead to biased state estimates, low accuracy, and loss of important information. The main goal of this research project is to investigate the impact of parameter estimation in state space models on the Kalman filter performance and propose improvements to increase the accuracy and efficiency of state estimation.

Supervisors and contacts: A. Manuela Gonçalves (UM|CMAT) and Marco Costa (CIDMA-Univ. Aveiro)

### Machine-assisted theorem proving

Case studies in developing the meta-theory of proof systems with the assistance of Coq.

Supervisors and contacts: José Espírito Santo (UM|CMAT) and Luís Pinto (UM|CMAT)

jes@math.uminho.pt; luis@math.uminho.pt

### Machine Learning Methods for Longitudinal Data Prediction

In longitudinal studies it is of great interest to make predictions for individual longitudinal trajectories. I this project we intend to compare the traditional likelihood methods and machine learning methods when using them for longitudinal data prediction. It is our hypothesis to observe better performance of machine learning methods with the increase of size in the data.

Supervisors and contacts: Inês Sousa (UM|CMAT)

### Modelling risks in extreme value theory

Modelling and assessing the risk of extreme events is important in many contexts. Risk measures are fundamental tools for that purpose. The aim of this project is to develop new risk measures in extreme value theory, taking into account tail based quantities of the underlying events’ distribution, such as the extreme value index or the mean excess.

The mathematical properties of the risk measures are analysed and the influence of the different tail parameters on the risk are investigated.

The risk measures will be applied to the financial context, in order to propose new tail based portfolio stock selection models.

Supervisors and contacts: Irene Brito (UM|CMAT) and Marta Ferreira (UM|CMAT)

ireneb@math.uminho.pt ; msferreira@math.uminho.pt

### Negative translations and call-by-value

Negative translations are interpretations of classical logic into intuitionistic logic. Under the Curry-Howard isomorphism, they correspond to continuation-passing style (CPS) translations, which are interpretations between functional programming languages following different calling paradigms. Recent results shows the essence of call-by-value CPS-translations is an interpretation into a specific sequent calculus, but these results do not extend yet to classical logic.

Supervisors and contacts: José Espírito Santo (CMAT)

### Nonlinear Partial Differential Equations

Nonlinear partial differential equations (pdes) model several physical and biological phenomena, being for that of great interest and relevance, and give rise to quite interesting and defiant questions. Many is done but there are still several questions to be answered (namely concerning anisotropic regimes and doubly nonlinear pdes).

This proposal of a PhD thesis comprehends a review of the literature (known results) and aims to point out open problems and to give a contribution to solve them; possibly in co-supervision with national or foreign collaborators.

Supervisors and contacts: Eurica Henriques (UTAD|CMAT)

### Optimization for Deep Learning

Neural networks (NN) are trained using a gradient method for finding the optimal weights (parameters) of the NN model that minimizes the loss function (model error). Although NN are a powerful model, in practice, it is hard to train properly and can be computationally expensive. Among the main reasons why these models are so unwieldy are: i) the dataset and the number of weights can both be very large in practice; ii) gradient method converges very slowly in optimizing NN with many weights; iii) NN can suffer from vanishing and exploding gradient problems. In this work, we propose to investigate and develop optimization methods to overcome these issues, that take into account the error backpropagation when training NN.

Supervisors and contacts: Fernanda Costa (UM|CMAT) and Luís L. Ferrás (UM|CMAT)

mfc@math.uminho.pt ; llima@math.uminho.pt

### Parameter estimation in state space models: development of advanced approaches and practical applications

State space models are widely used to describe complex dynamical systems in which the relationships between variables are expressed in terms of equations of state. The ability to accurately estimate the parameters of these models is essential for the proper identification and prediction of the variables involved. The goal of this research project is to develop advanced approaches for parameter estimation in state space models and investigate their practical applications in different areas of study. This study will seek to address the challenges associated with parameter estimation in complex models, considering the presence of noise, no-Gaussian distributions, nonlinearities, and other features.

Supervisors and contacts: A. Manuela Gonçalves (UM|CMAT) and Marco Costa (CIDMA-Univ. Aveiro)

### Pseudo-Riemannian geometry on homogenous manifolds

Lie groups, symmetric spaces or more generally homogenous manifolds are good model spaces for many problems arising in pseudo-Riemannian geometry. Under this topic, different projects can be proposed for a PhD thesis, according to the interest of the student, possibly in co-superivsion with a foreign collaborator.

Supervisors and contacts: Ana Cristina Ferreira (UM | CMAT)

### Statistical learning for spatial and temporal streaming data

Streams of data are all around us, and the need to process that data instantly —or as close to real time as possible— has become evident. This project addresses the problem of predicting spatio-temporal processes with temporal patterns that vary across spatial regions, when data is available as a stream, meaning that the dataset is augmented sequentially. The methods to be proposed must be evaluated using both synthetic and real data, hopefully demonstrating their ability to accurately predict data missing in spatial regions over time.

Supervisors and contacts: Raquel Menezes (UM|CMAT) and M. Eduarda Silva (FEP-UP|CIDMA-Univ. Aveiro)

### Time series and risk analysis for environmental quality assessment

This project intends to develop new methodologies, combining concepts from risk theory and times series modelling approaches, for the forecasting of environmental variables in the context of environmental quality assessment. The new proposed methodologies will be evaluated using both simulations studies and real data (e.g. water quality monitoring, air pollution monitoring).

Supervisors and contacts: A. Manuela Gonçalves and Irene Brito (UM|CMAT)

mneves@math.uminho.pt__; __ireneb@math.uminho.pt

### Topological complexity and related invariants

The project aims to study the notion of topological complexity and some of its approximations for certain classes of topological spaces using techniques from algebraic topology.

Supervisors and contacts: Lucile Vandembroucq (UM|CMAT)