<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></style> </head> <body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word"> <div class="WordSection1"> Hi everyone, On Monday, the MSP101 talk will be given by Conor McBride (MSP). See the details of the talk below.<o:p></o:p> Best, Dilsat ********************************************************************** Date: Monday, 20 January at 15:00 Room: LT412, Livingstone Tower Zoom link: <a href="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1" target="_blank" title="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1">https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1</a> Speaker: Conor McBride Title: My Favourite Double Category<o:p></o:p> Abstract: I'll (re)introduce the "codeBruijn" representation of syntax with binding, in which terms are intrinsically indexed over their support (the variables they are involved with) rather than their scope. These supports form the objects of a category of order-preserving injections ("thinnings" to MSP locals and "my triangle" to Blaise Pascal), whose dual ("selections") plays a crucial role in managing the restrictions of the variable support in specific substructures. Meanwhile, the notion of "simultaneous substitution" tightens to a relevant structure where every variable in the source support has an image, and every variable in the target support is used by at least one of those images. The action of substitution (which includes substitution composition) respects support precisely. It is reliant on the way a selection from a substitution's source support variables retains only some of their images and is itself relevant only once we have identified the corresponding selection from the target support of only those variables used in the retained images. We acquire squares with selections for vertical edges and relevant substitutions for horizontal edges which compose in both dimensions, forming a double category. (For anyone who saw, or for that matter, gave Phil Wadler's talk at the last SPLS, codeBruijn shifting happens at the root of a term, obviating the complex relationship between renaming and substitution which happens only because de Bruijn shifting happens at the leaves.) (For dependently typed programmers, more generally, there may be transferable lessons in managing coherence.)<o:p></o:p> **********************************************************************<o:p></o:p> </div> </body> </html>