<html> <head> <meta http-equiv="Content-Type" content="text/html; charset=windows-1253"> </head> <body> Hello, On Monday, the MSP101 talk will be given by Ohad Kammar (University of Edinburgh). See the details of the talk below. Best, Dilsat ********************************************************************** Date: Monday, 10 November at 13:00 Room: LT1414a, Livingstone Tower Zoom link: <a href="https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1" data-outlook-id="f973f694-ef87-4e0a-9bc4-ea8464b3b1fb" style="margin-top: 0px; margin-bottom: 0px;">https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1</a>  (Meeting ID 821 4378 8147, passcode whiteboard) Live stream on Youtube: <a href="https://www.youtube.com/@msp.strathclyde" data-outlook-id="022b293f-9708-43b6-bdc1-d5249a187c0b" style="margin-top: 0px; margin-bottom: 0px;">https://www.youtube.com/@msp.strathclyde</a> Speaker: Ohad Kammar (University of Edinburgh) Title: Modular abstract syntax trees (MAST) – substitution tensors with second-class sorts <div dir="ltr" class="MsoNormal" style="text-align: left; text-indent: 0px; margin: 0cm; font-family: Aptos, sans-serif; font-size: 11pt; color: black;"> </div> Abstract: We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value ë-calculus (CBV) and Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts means the presheaf of variables is no longer a left-unit for Fiore et al's substitution tensor product. We generalised their development to associative and right-unital skew monoidal categories. We reuse much of the development through skew bicategorical arguments. In ongoing work, we replace the skew monoidal structure with ordinary monoidal structure by recourse to substitution modules instead of substitution monoids. <div dir="ltr" style="font-family: Aptos, sans-serif; font-size: 11pt; color: rgb(0, 0, 0);"> </div> <div style="font-family: Aptos, sans-serif; font-size: 11pt; color: rgb(0, 0, 0);"> We apply the resulting theory in two scenarios. We employ the mathematical theory to circumvent the expression problem when proving substitution lemmata for varieties of CBV denotational semantics modularly. We employ a computational implementation of the theory to circumvent the expression problem when implementing intrinsically-typed foreign-function interfaces for the 29 theories of SMTLIB.</div> <div dir="ltr" style="font-family: Aptos, sans-serif; font-size: 11pt; color: rgb(0, 0, 0);"> </div> <div style="font-family: Aptos, sans-serif; font-size: 11pt; color: rgb(0, 0, 0);"> Joint work with Marcelo Fiore, Kajetan Granops, Mihail-Codrin Iftode, Georg Moser, and Sam Staton.</div> <div dir="ltr" class="MsoNormal" style="text-align: left; text-indent: 0px; margin: 0cm; font-family: Aptos, sans-serif; font-size: 11pt; color: rgb(0, 0, 0);"> </div> ********************************************************************** <div dir="ltr" style="font-family: Aptos, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);"> </div> </body> </html>