BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Liquid Haskell: Usable Language-Based Program Verif
 ication
DTSTART:20180319T101500
DTEND:20180319T113000
DTSTAMP:20260406T170224Z
UID:c65ab3edf05a057082370bd5c954e09e0ca21f8dd6171a4b6b9d9d92
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Niki Vazou - University of Maryland\nIC Faculty candidate\
 n\nAbstract:\nFormal verification has been gaining the attention and resou
 rces of both the academic and the industrial world since it prevents criti
 cal software bugs that cost money\, energy\, time\, and even lives. Yet\, 
 software development and formal verification are decoupled\, requiring ver
 ification experts to prove properties of a template – instead of the act
 ual – implementation ported into verification specific languages. My goa
 l is to bridge formal verification and software development for the progra
 mming language Haskell. Haskell is a unique programming language in that i
 t is a general purpose\, functional language used for industrial developme
 nt\, but simultaneously it stands at the leading edge of research and teac
 hing welcoming new\, experimental\, yet useful features.\nIn this talk I a
 m presenting Liquid Haskell\, a refinement type checker in which formal sp
 ecifications are expressed as a combination of Haskell’s types and expre
 ssions and are automatically checked against real Haskell code. This natur
 al integration of specifications in the language\, combined with automatic
  checking\, established Liquid Haskell as a usable verifier\, enthusiastic
 ally accepted by both industrial and academic Haskell users. Recently\, I 
 turned Liquid Haskell into a theorem prover\, in which arbitrary theorems 
 about Haskell functions would be proved within the language. As a conseque
 nce\, Liquid Haskell can be used in Haskell courses to teach the principle
 s of mechanized theorem proving.   \nTurning a general purpose language 
 into a theorem prover opens up new research questions – e.g.\, can theor
 ems be used for runtime optimizations of existing real-world applications?
  – that I plan to explore in the future.\n\nBio:\nNiki Vazou is a Postdo
 ctoral Fellow at the Programming Languages Group at University of Maryland
 . She completed her Ph.D at UC San Diego\, where together with her supervi
 sor Ranjit Jhala\, she developed Liquid Haskell\, a formal verifier integr
 ated into the Haskell programming language. During her Ph.D she was an int
 ern at MSR Cambridge\, MSR Redmond\, and Awake Security\, where she collab
 orated with top Haskell researchers and industrial developers on further e
 xpanding the applications and foundations of Liquid Haskell. Niki received
  the MSR Graduate Fellowship and is a member of the HaskellOrg committee.\
 n\nMore information\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR