CSAIL Event Calendar
PL/SE Seminar: HALO: Haskell to Logic through Denotational SemanticsSpeaker: Dimitrios Vytiniotis, Microsoft Research Date: Tuesday, November 13 2012 Time: 2:00PM to 3:30PM Location: 32-G449 (Patil/Kiva) Host: Adam Chlipala, CSAIL Contact: Adam Chlipala, adamc@csail.mit.edu Relevant URL: http://research.microsoft.com/en-us/people/dimitris/Even well-typed programs can go wrong in modern, typed, higher-order, functional languages, by encountering a pattern-match failure, or simply returning the wrong answer. An increasingly-popular response is to allow programmers to write contracts that express behavioural properties, such as crash-freedom or some useful post-condition. We study the static verification of such contracts. Our main contribution is a novel translation to first-order logic of both Haskell programs, and contracts written in Haskell, all justified by denotational semantics. This translation enables us to prove that functions satisfy their contracts using an off-the-shelf first-order logic theorem prover. In this talk I will describe (and demo) the sort of verification problems we can solve using our approach, but also explain challenges and future directions.
 
|