BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Practicality and Soundness of Refinement Types
DTSTART:20230928T140000
DTEND:20230928T150000
DTSTAMP:20260414T215229Z
UID:be5de30223f538929dec52d06751008a4b3be029bd32d97b85302924
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Niki Vazou\n\nAbstract\nRefinement types decorate the types
  of a programming language with logical predicates to allow rnore expressi
 ve type specifications. Originally\, refinement type based specifications 
 were restricted to SMT decidable theories arnd allowed automatic "light" v
 erification\, for example properties like non-division by zero or in-bound
  indexing. Verification of such light properties though requires "deeper" 
 specifications\, for example "is append associative?" or even "does your l
 anguage preserve typing?" In this talk\, I will present an overview of Liq
 uid Haskell's refinement types and discuss if they are practical\, general
 \, expressive\, and sound.\n\nBio\nNiki Vazou is an associate research pro
 fessor at IMDEA Software Institute. She works on verification of functiona
 l programming and the foundations and applications of refinement types. Ni
 ki did her PhD at uc San Diego where she developed liquid Haskell. She has
  received the Microsoft Research Fellowship and the ERC Starting Grant.\n\
 nMore information\n\nVideo
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410 https://epfl.zoom.us/
 j/61428727647
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR