BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Nachi Valliappan (University of Edinburgh)
DTSTART:20251003T130000Z
DTEND:20251003T140000Z
DTSTAMP:20260410T224605Z
UID:TheoryCSBham/54
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/TheoryCSBham
 /54/">Lax modal lambda calculi</a>\nby Nachi Valliappan (University of Edi
 nburgh) as part of University of Birmingham theoretical computer science s
 eminar\n\nLecture held in LC-UG10 Murray Learning Centre.\n\nAbstract\nInt
 uitionistic modal logic (IML) is the study of extending intuitionistic pro
 positional logic with modal operators such as the box and diamond modaliti
 es. Advances in IML have led to a plethora of useful applications in progr
 amming languages via the development of corresponding type theories with m
 odalities. Until recently\, IMLs with diamonds had been misunderstood as s
 omewhat peculiar and unstable\, causing the development of type theories w
 ith diamonds to lag behind type theories with boxes.\n\nIn this talk\, I w
 ill present a family of typed-lambda calculi corresponding to sublogics of
  a peculiar IML with diamonds known as Lax logic. These calculi provide a 
 modal logical foundation for strong functors in functional programming and
  make it possible to formalize the connection between possible-world seman
 tics for IMLs and categorical semantics for corresponding lambda calculi. 
 I hope to end this talk with a summary of what I’ve learnt from IML lite
 rature and how it has inspired me to think about semantics of modalities i
 n programming languages beyond boxes and diamonds. \n\nA draft article on 
 this topic can be found here: $\\url{https://nachivpn.me/lmlc.pdf}$\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/54/
END:VEVENT
END:VCALENDAR