BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Toward a liquid call-by-push-value - Dimitrios Economou (Universit
 y of Cambridge)
DTSTART:20250428T120000Z
DTEND:20250428T130000Z
UID:TALK229222@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
DESCRIPTION:Refinement typing algorithms are hard to design and understand
 . Liquid Haskell has practical and powerful features like modular\, recurs
 ive refinements of inductive data that are nonetheless guaranteed to gener
 ate SMT-decidable typing constraints. But Liquid Haskell is relatively har
 d to understand because it lacks an explicit phase distinction between ind
 ices and programs. Index-based systems like Dependent ML tend to be less p
 ractical\, especially since they aren't guaranteed to create SMT-decidable
  constraints\, but are easier to understand due to their index/program pha
 se distinction.\n\nIn this talk we discuss how to apply techniques from lo
 gic\, type theory\, and category theory to design a correct and straightfo
 rward bidirectional typing algorithm for modular\, recursive index refinem
 ents. We use focusing to design logically a call-by-push-value (CBPV) syst
 em with measures on inductive data. CBPV has good semantic properties even
  in the presence of computational effects. Bidirectional type systems are 
 a reliable way to combine type checking and inference\, with a straightfor
 ward initial recipe in sequent calculus. We prove that our declarative sys
 tem is operationally sound\, operationally complete (adequacy)\, and sound
  with respect to a standard denotational semantics\, all of which taken to
 gether imply logical consistency\, as well as total correctness both opera
 tionally and denotationally. We design an algorithmic system and prove it 
 is decidable\, sound\, and complete. Focusing and bidirectional typing com
 bine nicely with a new concept that seems to be exploited in liquid type s
 ystems: value-determined existential indices of input types under focus ar
 e guaranteed to be solvable at the end of focusing\, outputting existentia
 l-free types and constraints decidable by an SMT solver.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR