<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">We’re gonna be kicking off our MSP101 this semester with a talk from Conor McBride on Monday! Hope to see you there.<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 19<sup>th</sup> January, 1:00 pm, Livingstone Tower room LT210<br>
<br>
Speaker:<br>
Conor McBride (MSP)<br>
<br>
Title:<br>
Wiggle It (Just a Little Bit)<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>
Abstract:<br>
Testing can reveal the absence of bugs in situations where we can show that the test data expose all the possible variations. This is straightforward when the domain is finite, but one can also achieve test coverage for large domains by restricting the ways
in which the program may process its input. For example, the fact that the sum of the numbers less than n is n choose 2 can be proven by testing for n in {0, 1, 2} because both calculations are inherently quadratic. I have, on and off, been thinking about
how to deliver similar results for other inductive data structures. For example, one can generate particularly well behaved folds on unlabelled binary trees by giving (i) the tree which is the image of the leaf, and (ii) a tree with two variables showing how
the ouptut for a node is computed from the outputs for its two subtrees. I claim that if two such folds agree at the four smallest trees, then they agree for all trees. Clearly, we recover (i) by testing at a leaf. We recover (ii) by testing at a node with
leaves for subtrees, then perturbing each of those subtrees in turn, to see where the output changes. That is to say, we use perturbation to recover abstraction. I am currently working on a proof of this claim in Agda and will share my progress (and my prospectus)
in this talk.<o:p></o:p></p>
<p class="MsoNormal">----------------------------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>