Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Sobre
Download foto HD

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

    Portugal
  • Contactos

    +351253604440
    jose.n.oliveira@inesctec.pt
003
Publicações

2018

Programming from metaphorisms

Autores
Oliveira, JN;

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

Abstract
This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.

2017

The data cube as a typed linear algebra operator

Autores
Oliveira, JN; Macedo, HD;

Publicação
ACM International Conference Proceeding Series

Abstract
There is a need for a typed notation for linear algebra applicable to the ields of econometrics and data mining. In this paper we show that such a notation exists and can be useful in formalizing and reasoning about data aggregation operations. One such operation - the construction of a data cube - is shown to be easily expressible as a linear algebra operator. The construction is shown to be type-generic and some of its properties are derived from its typed deinition and proved using matrix algebra. Other forms of data aggregation such as eg. rollup and cross tabulation are shown to be algebraically derivable from data cubes. © 2017 Association for Computing Machinery.

2017

Computer Aided Verification of Relational Models by Strategic Rewriting

Autores
Necco, CM; Oliveira, JN; Visser, J; Uzal, R;

Publicação
JOURNAL OF COMPUTER SCIENCE & TECHNOLOGY

Abstract
Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a type-directed, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.

2016

"Keep definition, change category" - A practical approach to state-based system calculi

Autores
Oliveira, JN; Miraldo, VC;

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

Abstract
Faced with the need to quantify software (un)reliability in the presence of faults, the semantics of state-based systems is urged to evolve towards quantified (e.g. probabilistic) nondeterminism. When one is approaching such semantics from a categorical perspective, this inevitably calls for some technical elaboration, in a monadic setting. This paper proposes that such an evolution be undertaken without sacrificing the simplicity of the original (qualitative) definitions, by keeping quantification implicit rather than explicit. The approach is a monad lifting strategy whereby, under some conditions, definitions can be preserved provided the semantics moves to another category. The technique is illustrated by showing how to introduce probabilism in an existing software component calculus, by moving to a suitable category of matrices and using linear algebra in the reasoning. The paper also addresses the problem of preserving monadic strength in the move from original to target (Kleisli) categories, a topic which bears relationship to recent studies in categorial physics.

2015

A linear algebra approach to OLAP

Autores
Macedo, HD; Oliveira, JN;

Publicação
FORMAL ASPECTS OF COMPUTING

Abstract
Inspired by the relational algebra of data processing, this paper addresses the foundations of data analytical processing from a linear algebra perspective. The paper investigates, in particular, how aggregation operations such as cross tabulations and data cubes essential to quantitative analysis of data can be expressed solely in terms of matrix multiplication, transposition and the Khatri-Rao variant of the Kronecker product. The approach offers a basis for deriving an algebraic theory of data consolidation, handling the quantitative as well as qualitative sides of data science in a natural, elegant and typed way. It also shows potential for parallel analytical processing, as the parallelization theory of such matrix operations is well acknowledged.

Teses
supervisionadas

2019

Rust para Sistemas Críticos

Autor
André Brandão de Pinho

Instituição
UM

2018

Towards Quantum Program Calculation

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2017

Pointfree Program Calculation — Theory and Applications

Autor
Claudia Monica Necco

Instituição
UM

2016

Pointfree Program Calculation — Theory and Applications

Autor
Claudia Mónica Necco

Instituição
UM

2015

Automatic Rewrite Proofs by Reflection in Agda

Autor
Victor Cacciari Miraldo

Instituição
UM