Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About

About

I am professor of Computer Science at the Informatics Department of University of Minho and researcher at HASLab/ INESC TEC. I am also a member of IFIP WG 2.1 (Algorithmic Languages and Calculi) and of the Formal Methods Europe (FME) Association. I serve on the editorial board of Springer journal Formal Aspects of Computing.
RESEARCH 
My research interests are focussed on formal methods, algebra of programming (program calculation) and functional programming. I've published recently on relation algebra and its application to programming. Currently, I am developing a linear algebra of programming which I want to apply to the verification of complex software systems, including quantum ptogramming.

Interest
Topics
Details

Details

  • Name

    José Nuno Oliveira
  • Role

    Research Coordinator
  • Since

    01st November 2011
004
Publications

2025

Logic and Calculi for All on the occasion of Luis Barbosa's 60th birthday

Authors
Madeira, A; Oliveira, JN; Proença, J; Neves, R;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
[No abstract available]

2025

Introduction to the Special Collection from FACS 2022

Authors
Tapia Tarifa, SL; Proença, J; Oliveira, JN;

Publication
Formal Aspects Comput.

Abstract
[No abstract available]

2025

How much is in a square? Calculating functional programs with squares

Authors
Oliveira, JN;

Publication
JOURNAL OF FUNCTIONAL PROGRAMMING

Abstract
Experience in teaching functional programming (FP) on a relational basis has led the author to focus on a graphical style of expression and reasoning in which a geometric construct shines: the (semi) commutative square. In the classroom this is termed the magic square (MS), since virtually everything that we do in logic, FP, database modeling, formal semantics and so on fits in some MS geometry. The sides of each magic square are binary relations and the square itself is a comparison of two paths, each involving two sides. MSs compose and have a number of useful properties. Among several examples given in the paper ranging over different application domains, free-theorem MSs are shown to be particularly elegant and productive. Helped by a little bit of Galois connections, a generic, induction-free theory for ${\mathsf{foldr}}$ and $\mathsf{foldl}$ is given, showing in particular that ${\mathsf{foldl} \, {{s}}{}\mathrel{=}\mathsf{foldr}{({flip} \unicode{x005F}{s})}{}}$ holds under conditions milder than usually advocated.

2024

Alloy Goes Fuzzy

Authors
Silva, P; Cunha, A; Macedo, N; Oliveira, JN;

Publication
RIGOROUS STATE-BASED METHODS, ABZ 2024

Abstract
Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.

2024

On the Relational Basis of Early R/G Work

Authors
Oliveira, N;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
The R/G approach to the development of interfering programs was initiated by the pioneering work of Cliff Jones (1981) on a relational basis. R/G has been the subject of much research since then, most of it deviating from the original relational set-up. This paper looks at such early work from a historical perspective and shows how it can be approached and extended using state-of-the-art relational algebra. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.

Supervised
thesis

2023

Towards a typed linear algebra formal semantics for spreadsheets

Author
Rui Filipe Brito Azevedo

Institution
UM

2023

Functional Programming for Explainable AI

Author
Gonçalo José Azevedo Esteves

Institution
UM

2023

Towards ‘Just Good Enough’ Quantum Programming

Author
Ana Isabel Carvalho Neri

Institution
UM

2023

Verificação e descoberta de modelos probabilísticos no Alloy Analyser.

Author
Pedro Faria Durães da Silva

Institution
UM

2022

Processamento Analítico com Álgebra Linear Tipada em MonetDB

Author
Lucas Ribeiro Pereira

Institution
UM