BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Bryce Goldman (Topos Institute)
DTSTART:20261105T213000Z
DTEND:20261105T221500Z
DTSTAMP:20261030T095303Z
UID:ThirdVWDC/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ThirdVWDC/3/
 ">A Programming Language for Virtual Double Theories</a>\nby Bryce Goldman
  (Topos Institute) as part of Third Virtual Workshop on Double Categories\
 n\n\nAbstract\nLike familiar theories of first-order logic\, the theories 
 of many categorical logics can be specified by a finite presentation of ge
 nerating symbols and axioms. Each categorical logic is parameterized by a 
 "virtual double theory"\, a kind of virtual equipment\, which can be used 
 to construct type theories over their models. This is especially useful in
  software systems based on categorical logic\, such as CatColab\, where mo
 dels of various domain-specific logics are supported by type systems built
  uniformly from these virtual double theories.\n\nBuilding on prior work b
 y Hayato Nasu on a type theory for virtual double categories\, we introduc
 e foundations for a programming language for specifying virtual double the
 ories\, and present a prototype compiler. We highlight connections with or
 dered linear logic\, and propose a novel operational semantics that captur
 es the universal properties of loose units through a directed reduction pr
 ocedure.\n
LOCATION:https://researchseminars.org/talk/ThirdVWDC/3/
END:VEVENT
END:VCALENDAR