Date: September 27

Venue: University of Minho, Gualtar campus (Braga) | Informatics Department, Building 07 | Auditorium 2, first floor

Time: 2pm

Presenter: José N. Oliveira - HASLab, INESC TEC & University of Minho

Title: The Data Cube as a Typed Linear Algebra Operator - The verified OCaml Library

More info HERE

Abstract: There is a need for a typed notation in linear algebra applicable to the fields of econometrics and data mining. This talk will show that such a notation exists and is useful in formalizing and reasoning about data aggregation operations. In particular, one such operation — the construction of a data cube — is shown to be easily expressible as a linear algebra operator. The construction is type-generic and its properties, which can be derived from its typed definition using matrix algebra, include a “free theorem”. Linearity also ensures incremental updating of data cubes in face of raw data updates. The construction is “universal” in the sense that the other forms of data aggregation (eg. slicing, rollup, cross tabulation, etc) are algebraically derivable from the given linear algebra definition of cubes, in a way that is amenable to parallelization.

Short bio: José N. Oliveira is a full professor of Computer Science at the Informatics Department of University of Minho and researcher at HASLab/INESC TEC. He is also a member of IFIP WG 2.1 (Algorithmic Languages and Calculi) and of the Formal Methods Europe (FME) Association; and also serves on the editorial board of Springer journal Formal Aspects of Computing. José's research interests are focused on formal methods, algebra of programming (program calculation) and functional programming. Throughout his career, José published tens of book chapters, journals, and other peer-reviewed publications on relation algebra and its application to programming since three decades. He also served as PC member for over 50 venues. Currently, he is developing a linear algebra of programming which he wants to apply to the verification of complex software systems.