[msp-interest] [MSP101] Georgi Nakov: Matrix Typing Rules (1pm Mon 3/11, LT1414a)

[Fiona Blackett]

Hello all,

Next Monday we will have our MSP101 talk, titled Matrix Typing Rules, and given by Georgi Nakov. See below for details!

Cheers,
Fiona Blackett
----------------------------------------------------------------------------------------------

Date, time and place:
 Monday 3rd November, 1:00 pm, Livingstone Tower room LT1414a

Speaker:
  Georgi Nakov (MSP)

Title:
  Matrix Typing Rules

Zoom Link:
  https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1
  Meeting ID: 821 4378 8147
  Password: whiteboard


Abstract:
What is an appropriate type for a matrix, and what are the accompanying typing rules? Depending on your mileage, the answer might seem obvious or dull - can't we start with a humble $\mathsf{Matrix}\,A\,m\,n$? I would argue that better candidates exist, and that suitable typing rules are far from obvious, at least if we aim at actually implementing the said rules. In this talk, I will embark on the long journey of turning something that looks good on paper into something that works in code. We try to abolish any implicit assumptions, hidden computation and blind guessing from the initial typing rules, and refine them until they can guide a precise implementation. With guest occurrences of the usual suspects - bidirectional typing, thinnings, and typecheckers-that-get-to-know-monoid-laws.
----------------------------------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20251030/db02233f/attachment.html