InfoBlender Webinar

Type Your Matrices for Great Good | Armando Santos

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.

Biography:

I am currently finishing my Master degree at University of Minho, and a Research Assistant at INESC TEC. My specializations are in the areas of Formal Methods in Software Engineering and Distributed Systems, but my research interest covers algebra of programming, functional programming, abstract maths, and lately applying semantic elegance and rigour to library design. My master thesis topic is about "Selective Functors & Probabilistic Programming", where I am using Haskell, Selective Functors and static analysis to explore what can be done with this new functional abstraction in the probabilistic setting.

Notes:

Please register here until December 14, in order to have access to the link for the Zoom session. The webinar will be recorded.