[msp-interest] [MSP101] Sean Watters: What I did in my PhD (1pm Mon 27/10, LT310)

[Fiona Blackett]

Hello all,

Next Monday Sean will be giving our MSP101 talk, on what he did during his PhD!

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

Date, time and place:
 Monday 27rd October, 1:00 pm, Livingstone Tower room LT310

Speaker:
  Sean Watters (MSP)

Title:
  What I did in my PhD

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

Abstract:
  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.

    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.

----------------------------------------------------------------------------------------------

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