<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:12.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hello all,<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">Next Monday we will have our MSP101 talk, titled Matrix Typing Rules, and given by Georgi Nakov. See below for details!<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">Cheers, <o:p></o:p></p>
<p class="MsoNormal">Fiona Blackett <o:p></o:p></p>
<p class="MsoNormal">----------------------------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">Date, time and place:<br>
Monday 3rd November, 1:00 pm, Livingstone Tower room LT1414a<br>
<br>
Speaker:<br>
Georgi Nakov (MSP)<br>
<br>
Title:<br>
Matrix Typing Rules<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">Zoom Link: <o:p></o:p></p>
<p class="MsoNormal"> <a href="https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1">https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1</a><o:p></o:p></p>
<p class="MsoNormal"> Meeting ID: 821 4378 8147<o:p></o:p></p>
<p class="MsoNormal"> Password: whiteboard<br>
<br>
<br>
Abstract:<br>
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. <o:p></o:p></p>
<p class="MsoNormal">----------------------------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>