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
Publications

Publications by José Nuno Oliveira

2015

Relational and Algebraic Methods in Computer Science 15th International Conference, RAMiCS 2015 Braga, Portugal, September 28-October 1, 2015 Proceedings

Authors
Kahl, W; Winter, M; Oliveira, JN;

Publication
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2015)

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.

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.

2020

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

Authors
Santos, A; Oliveira, JN;

Publication
Haskell 2020 - Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2020

Abstract
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory. © 2020 ACM.

2019

Formal Methods – The Next 30 Years

Authors
ter Beek, MH; McIver, A; Oliveira, JN;

Publication
Lecture Notes in Computer Science

Abstract

2020

Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I

Authors
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;

Publication
FM Workshops (1)

Abstract

  • 3
  • 11