BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Andrés Viso (Software Heritage\, France and UNQ\, Argentina)
DTSTART:20210527T170000Z
DTEND:20210527T180000Z
DTSTAMP:20260423T052451Z
UID:LoReL/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/4/">En
 coding Tight Typing in a Unified Framework</a>\nby Andrés Viso (Software 
 Heritage\, France and UNQ\, Argentina) as part of LoReL Seminar\n\n\nAbstr
 act\nThis joint work with Delia Kesner explores how the intersection type 
 theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a
  more general framework provided by call-by-push-value (CBPV). Indeed\, we
  propose tight type systems for CBN and CBV that can be both encoded in a 
 tight type system for CBPV. All such systems are quantitative\, in the sen
 se that they provide exact information about the length of normalization s
 equences to normal form as well as the size of these normal forms. Moreove
 r\, the length of sequences to normal forms are discriminated according to
  their multiplicative/exponential nature\, a concept inherited from linear
  logic.\n
LOCATION:https://researchseminars.org/talk/LoReL/4/
END:VEVENT
END:VCALENDAR