BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Ohad Kammar (University of Edinburgh)
DTSTART:20251024T130000Z
DTEND:20251024T140000Z
DTSTAMP:20260403T223300Z
UID:TheoryCSBham/56
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/TheoryCSBham
 /56/">Modular abstract syntax trees (MAST) – substitution tensors with s
 econd-class sorts</a>\nby Ohad Kammar (University of Edinburgh) as part of
  University of Birmingham theoretical computer science seminar\n\nLecture 
 held in LG23\, Computer Science.\n\nAbstract\nWe adapt Fiore\, Plotkin\, a
 nd Turi's treatment of abstract syntax with binding\, substitution\, and h
 oles to account for languages with second-class sorts. These situations in
 clude programming calculi such as the Call-by-Value λ-calculus (CBV) and 
 Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appe
 aring in variable contexts means the presheaf of variables is no longer a 
 left-unit for Fiore et al's substitution tensor product. We generalised th
 eir 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 monoid
 al structure by recourse to substitution modules instead of substitution m
 onoids.\n\nWe apply the resulting theory in two scenarios. We employ the m
 athematical theory to circumvent the expression problem when proving subst
 itution lemmata for varieties of CBV denotational semantics modularly. We 
 employ a computational implementation of the theory to circumvent the expr
 ession problem when implementing intrinsically-typed foreign-function inte
 rfaces for the 29 theories of SMTLIB.\n\nJoint work with Marcelo Fiore\, K
 ajetan Granops\, Mihail-Codrin Iftode\, Georg Moser\, and Sam Staton.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/56/
END:VEVENT
END:VCALENDAR