<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=iso-8859-1">
<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;
        panose-1:2 11 0 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        font-size:11.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;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:11.0pt;
        mso-ligatures:none;
        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"><span style="color:black">Hi all,<br>
<br>
On Monday, the MSP101 talk will be given by André Videla (MSP). See the details of the talk below.<o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black"><br>
Best,<br>
Dilsat<br>
<br>
**********************************************************************<br>
<br>
Date:&nbsp;Monday, 27 January at 15:00<br>
<br>
Room:&nbsp;LT412, Livingstone Tower<br>
<br>
Zoom link:&nbsp;<a href="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1" target="_blank" title="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1"><span style="color:#96607D">https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1</span></a><br>
<br>
Speaker:&nbsp;André Videla<br>
<br>
Title: Pipelining and dependent types<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="color:black">Abstract: Pipelining is a crude CPU optimisation to speed up execution of sequential programs. By allowing the manipulation of types as values, dependent types enable new abstractions to manipulate large-scale
 of software based on sequential computation inspired by CPU pipelining. I will show how to define pipelines, sequential programs that cannot easily be parallelised using a list of types as a specification. Given this list of type, the implementation of a pipeline
 is given by the functions between each type. This pipeline abstraction can be generalised to categories such that the pipeline is made up of objects and its implementation is given by the morphisms between them. This enable the use of kleisli morphisms for
 effectful programs. The pipeline can be further abstracted over graded categories enabling automatic composition of errors. Finally, I will show how to use dependent pipelines to allow composition of programs with type-dependency. An architecture particularly
 useful for single-pass compilers with well-scoped and well-typed implementations.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><br>
**********************************************************************<o:p></o:p></span></p>
<p class="MsoNormal"><o:p>&nbsp;</o:p></p>
</div>
</body>
</html>