LFCS Seminar: Dmitrios Vytiniotis
Static contract checking for Haskell through FOL semantics
What 


When 
Mar 20, 2012 from 04:00 PM to 05:00 PM 
Where  IF 4.3133 
Add event to calendar 
vCal iCal 
Any serious program contains assertions or documented function pre and postconditions. An alternative way to express such executable specifications is through contracts. In the context of Haskell, contracts have a welldefined operational semantics, but previous work does not settle the subject of statically checking contracts, expressed as ordinary programs, in an effective and practical way for a lazy functional language. In this work (in progress) we aim to address the problem taking a denotational semantics approach: We express the semantics of programs and of contracts directly in terms of firstorder logic formulae and automatically discharge the proof obligations that arise using a firstorder logic theorem prover. We show how we leverage the purity of Haskell for equational reasoning, how we use information from countermodels, how to avoid the search space explosion in the theorem prover, and how induction can possibly work. I will also demonstrate our ideas with a demo of our prototype implementation and sketch extensions to other features of the Haskell language, such as type classes.