<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-7">
<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 Sean will be giving our MSP101 talk, on what he did during his PhD!<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 27rd October, 1:00 pm, Livingstone Tower room LT310<br>
<br>
Speaker:<br>
Sean Watters (MSP)<br>
<br>
Title:<br>
What I did in my PhD<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<o:p></o:p></p>
<p class="MsoNormal"><br>
Abstract:<br>
The modal ì-calculus is a modal logic that type theorists don't usually spare much thought for; it's usually treated classically, and its main application is as a specification language for model checking, where it subsumes weaker but more commonly used logics
like LTL, CTL, and PDL. Meanwhile, modal logicians study the ì-calculus using very "1930s" concepts like explicitly named variables. Most of my efforts during my PhD have been spent trying to pull the theory of the modal ì-calculus into this century (AKA into
Agda) using the tools of type theory, but my real interest is in what we type theorists might glean from the exchange. For example, the modal ì-calculus is a fixpoint logic, with a very mature account of fixpoint alternation - something that every proof assistant
(to my knowledge) is lacking.<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"> In this talk, I'll be using the ì-calculus and some of my recent work on it as a motivating example to give a slightly non-standard introduction to some important MSP ideas - syntaxes with binding, and data types as fixpoints. I'll
cover the least fixpoint (which computer scientists love), the greatest fixpoint (which we sometimes tolerate), and the rational fixpoint (which many forget exists, but plays a key role in my work). If time permits, I'd also like to open the door to the terrifying
world of arbitrary fixpoint alternation, and some (very very early) ideas for taming it.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">----------------------------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>