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

    Informática
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
003
Publicações

2022

A tribute to Jose Manuel Valenca

Autores
Oliveira, JN; Pinto, JS; Barbosa, LS; Henriques, PR;

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

Abstract
The present Special Issue of the Journal of Logical and Algebraic Methods in Programming was planned as a tribute to Jose Manuel Esgalhado Valenca on the occasion of his Jubilation. A tribute to a professor, in the deepest sense of the word, a colleague and a friend, but above all to a long and inspiring academic journey that has so profoundly shaped the development of Informatics as a scientific area in Portugal. A scientific area that, as he taught us, needs to be understood broadly: not only as an independent research domain, but also as an educational pillar, a strategy for social and economic development, a foundation for a multifaceted professional career. This preface introduces some steps of such a journey. The Special Issue features a selection of scientific papers written by his collaborators, colleagues and friends, covering the different areas Jose Valenca helped to launch and consolidate in Portugal, namely computational logic, verification and mechanized reasoning, and information security. (c) 2022 Published by Elsevier Inc.

2022

Compiling Quantamorphisms for the IBM Q Experience

Autores
Neri, A; Barbosa, RS; Oliveira, JN;

Publicação
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

Abstract
Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of 'quantamorphism', a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits - often quite large - exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.

2020

Type your matrices for great good: a Haskell library of typed matrices and applications (functional pearl)

Autores
Santos, A; Oliveira, JN;

Publicação
Haskell 2020 - Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2020

Abstract

2020

Formal Methods. FM 2019 International Workshops

Autores
Sekerinski, E; Moreira, N; Oliveira, JN; Ratiu, D; Guidotti, R; Farrell, M; Luckcuck, M; Marmsoler, D; Campos, J; Astarte, T; Gonnord, L; Cerone, A; Couto, L; Dongol, B; Kutrib, M; Monteiro, P; Delmas, D;

Publicação
FM Workshops (1)

Abstract

2020

Formal Methods. FM 2019 International Workshops

Autores
Sekerinski, E; Moreira, N; Oliveira, JN; Ratiu, D; Guidotti, R; Farrell, M; Luckcuck, M; Marmsoler, D; Campos, J; Astarte, T; Gonnord, L; Cerone, A; Couto, L; Dongol, B; Kutrib, M; Monteiro, P; Delmas, D;

Publicação
FM Workshops (2)

Abstract

Teses
supervisionadas

2021

Towards ‘Just Good Enough’ Quantum Programming

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2021

Monitorização e Controlo de aplicações na nuvem

Autor
Daniel António Landeira da Silva

Instituição
UM

2020

Towards ‘Just Good Enough’ Quantum Programming

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2019

Rust para Sistemas Críticos

Autor
André Brandão de Pinho

Instituição
UM

2018

Especificação do modelo de folha de cálculo avançada

Autor
Ligia Iolanda Macedo Chiuale

Instituição