Who we are

The MiST research group focuses on the areas of programming languages, artificial intelligence, and software engineering, combining theoretical developments with practical applications. Since its creation, the members of the group have often collaborated with renowned researchers both from Spain and abroad, participating regularly in R&D projects and conferences.

Research Lines

• 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.

MiST website