Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Sobre

Sobre

Sou professor no Departamento de Informática da Universidade do Minho e investigador do HASLab / INESC TEC. Também sou membro do IFIP WG 2.1 (Algorithmic Languages and Calculi) e da Associação Formal Methods Europe (FME). Faço parte do conselho editorial da revista Formal Aspects of Computing da Springer.

Meus interesses de investigação estão focados em métodos formais, álgebra de programação (cálculo de programas) e programação funcional. Publiquei recentemente sobre álgebra de relações e sua aplicação à programação. Atualmente, estou a desenvolver uma álgebra linear de programação que quero aplicar à verificação de sistemas de software complexos tolerantes a falhas.

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    José Nuno Oliveira
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
004
Publicações

2025

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

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

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
[No abstract available]

2025

Introduction to the Special Collection from FACS 2022

Autores
Tarifa, SLT; Proenca, J; Oliveira, J;

Publicação
FORMAL ASPECTS OF COMPUTING

Abstract
[No abstract available]

2025

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

Autores
Oliveira, JN;

Publicação
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

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

Publicação
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

Autores
Oliveira, N;

Publicação
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.

Teses
supervisionadas

2023

Towards a typed linear algebra formal semantics for spreadsheets

Autor
Rui Filipe Brito Azevedo

Instituição
UM

2023

Functional Programming for Explainable AI

Autor
Gonçalo José Azevedo Esteves

Instituição
UM

2023

Towards ‘Just Good Enough’ Quantum Programming

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2023

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

Autor
Pedro Faria Durães da Silva

Instituição
UM

2022

Processamento Analítico com Álgebra Linear Tipada em MonetDB

Autor
Lucas Ribeiro Pereira

Instituição
UM