Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • 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
  • Cluster

    Computer Science
  • Role

    Research Coordinator
  • Since

    01st November 2011
Publications

2018

Programming from metaphorisms

Authors
Oliveira, JN;

Publication
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

Authors
Oliveira, JN; Macedo, HD;

Publication
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

Implementing a Linear Algebra Approach to Data Processing

Authors
Pontes, R; Matos, M; Oliveira, JN; Pereira, JO;

Publication
Lecture Notes in Computer Science - Grand Timely Topics in Software Engineering

Abstract

2017

Computer Aided Verification of Relational Models by Strategic Rewriting

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

Publication
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

Authors
Oliveira, JN; Miraldo, VC;

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

Supervised
thesis

2015

Benchmarking de uma abordagem em álgebra linear a sistemas OLAP

Author
Rogério António da Costa Pontes

Institution
UM

2015

Automatic Rewrite Proofs by Reflection in Agda

Author
Victor Cacciari Miraldo

Institution
UM

2015

Pointfree Program Calculation — Theory and Applications

Author
Claudia Monica Necco

Institution
UM