Research interests
The MiST research group is focused on different aspects of
programming languages, combining both theoretical developments and
practical applications. You can find below a summary of our main
research interests:
- Declarative formalisms. Declarative formalisms provide a high level of abstraction
and can be used both as specification and programming languages. We work on term rewriting,
logic programming (e.g., Prolog), functional programming (e.g., Haskell, Lean), and the
actor model (e.g., Erlang).
- Hybrid artificial intelligence. We combine declarative, rule-based formalisms (such as
logic programming and term rewriting) with probabilistic information—often learned from data—to
model uncertainty. Our approaches yield probabilistic models that are both formally verifiable
and interpretable. More recently, we have also explored so-called neurosymbolic AI.
- Software verification, testing, and debugging. Ensuring the reliability of critical
software is one of today’s key challenges. We explore formal verification techniques
(e.g., static analysis, model checking), software testing (e.g., concolic testing), and
debugging methods (e.g., program slicing). More recently, we have started using AI agents
to formalize properties and verify them using theorem provers such as Lean.
- Reversible computation. Reversible computation is relevant not only from a theoretical
perspective but also for applications such as bidirectional program transformation and
quantum computing. It also provides a path toward ultra-low-power computing by avoiding the
energy cost of information loss (Landauer's principle). We have defined reversible semantics
for languages such as Janus and Erlang, and developed a causally consistent reversible debugger
(CauDEr) for Erlang.
- Web information retrieval. Extracting useful information from the web benefits both
users and automated systems. For example, we study techniques to isolate main content by
removing boilerplate elements (ads, templates, banners), as well as methods for improving web indexing.
- Program transformation techniques. Program transformation techniques help improve efficiency,
readability, and other quality aspects of software. They are grounded in solid mathematical
foundations, enabling formal correctness guarantees.
Current members
Former members
Some (past and present) collaborators
Research Projects
The MiST research group is currently
involved in the following R+D projects:
- SAFER (4 years,
from June, 2020 to May, 2024) Funded
by EU (FEDER) and the Spanish MCI/AEI,
grant PID2019-104735RB-C41.
Analysis and Validation of Software and Web Resources
In collaboration with the
Babel,
Dec-Tau,
Smile,
and
ISG
groups.
- MERINET (4 years,
from Jan 1, 2017 to Dec 31, 2020) Funded
by Spanish MINECO/AEI and EU (FEDER),
grant TIN2016-76843-C4-1-R.
Rigorous Methods for the Future
Internet
In collaboration with the Dec-Tau
and Smile
groups.
- TAILOR (Foundations of Trustworthy AI - Integrating Reasoning, Learning and Optimization). ICT-48 H2020-RIA-952215 (from 2020 to 2023).
- COST
action IC1405 on Reversible
Computation - Extending Horizons of
Computing (from 2015 to 2019).
- FassLow (Fast and Slow Learning and Reasoning Technologies, CIPROM/2022/6), 2023-2026.
- PROMETEO/2019/098 DeepTrust: Deep Logic Technology for Software Trustworthiness (Excellence Research Group GV, 2019-2022)
- PROMETEOII/2015/013 SmartLogic:
Tecnologías Lógicas para
la Seguridad, Modelado, Análisis y Rendimiento del software
Software
You can check the group's
repository here. Some
additional tools can be found in the personal
pages of the members of the group.
