[msp-interest] [MSP101] Ohad Kammar: Modular abstract syntax trees (MAST) – substitution tensors with second-class sorts(LT1414a, 1pm Mon 10-Nov)

[Dilsat Yuksel]

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: https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1  (Meeting ID 821 4378 8147, passcode whiteboard)
Live stream on Youtube: https://www.youtube.com/@msp.strathclyde

Speaker: Ohad Kammar (University of Edinburgh)

Title: Modular abstract syntax trees (MAST) – substitution tensors with second-class sorts

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.

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.

Joint work with Marcelo Fiore, Kajetan Granops, Mihail-Codrin Iftode, Georg Moser, and Sam Staton.

**********************************************************************

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