[msp-interest] Re: [MSP101] Conor Mc Bride: Leftovers, Rightunders: Typechecking Thinnings Compositionally (1pm Mon 22/9, LT1310)

[Fredrik Nordvall Forsberg]

Clearly I don't remember how to do these announcements any more, as I 
forgot to include the Zoom link for online participation. Here it is:

Zoom link:
https://strath.zoom.us/j/82789104686?pwd=g1w5LFa4glTCFHzZbIKPX5qIBVEaKs.1

    (Meeting ID 827 8910 4686, passcode whiteboard)

Don't worry, Fiona will take over more competently from next week onwards.

Cheers,
Fred

On 19/09/2025 16:36, Fredrik Nordvall Forsberg wrote:
> Comrades,
>
> We kick off a new semester of the MSP101 seminar with a talk by Conor.
> The regular time for the coming semester is Mondays at 1pm.
>
> Hope to see you there!
>
> Cheers,
> Fred
>
>
> Date, time and place:
>     Monday 22 September, 13:00, Livingstone Tower room LT1310
>
> Speaker:
>     Conor Mc Bride (MSP)
>
> Title:
>     Leftovers, Rightunders: Typechecking Thinnings Compositionally
>
> Abstract:
>     In the interests of sharing MSP lore, I came up with a way to talk
>     about both the "Input Subject Output" approach to typechecking and the Category of
>     Thinnings in the same talk, making the latter an interesting example of the former.
>
>     The Input Subject Output approach, like most bidirectional approaches
>     to problem decomposition, tracks whether signals go from parent to child or vice
>     versa, but it also acknowledges a signal has a guarantor as well as a sender,
>     responsible for the meaningfulness of the signal. Meanwhile, thinnings are
>     order-preserving embeddings between ordered sequences, or dually, selections
>     of elements from sequences (their resemblance to binomial coffecients
>     is no accident), and are thus a fine example of a monoidal category.
>
>     I won't assume that any of you know know any of this: many of us do;
>     more of us should. And I'll try to tell the story with pictures, drawn on a
>     whiteboard, rather than jargon.
>
>     I often use thinnings to talk about embeddings between scopes, the
>     latter seen as sequences which grow on the right (because of prejudices about
>     time). A compositional way to typecheck a thinning is to start with the
>     available stuff "over" the thinning, together with a thinning that will start
>     choosing from the newest stuff on the right. If all is well, we shall learn which
>     "leftovers" have not yet been considered, and which "rightunders" have been not only
>     considered but also selected. There is a healthy story about both the
>     monoidal/parallel/spatial/tensor structure of thinnings and their
>     categorical/sequential/temporal/composition structure, yielding an
>     algorithm which never has to guess where to chop sequences in two.
>
> MSP101 Feeds:
>     Web: http://msp.cis.strath.ac.uk/msp101.html
>     RSS: http://msp.cis.strath.ac.uk/msp101.rss
>     iCal: http://msp.cis.strath.ac.uk/msp101.ics
>
>
>
> _______________________________________________
> msp-interest mailing list
> msp-interest at lists.strath.ac.uk
> http://lists.strath.ac.uk/mailman/listinfo/msp-interest