[PRL] Fwd: [MIT-PL] TALK:Tuesday 11-13-12 PL/SE Seminar: HALO: Haskell to Logic through Denotational Semantics

David Van Horn dvanhorn at ccs.neu.edu
Mon Nov 5 18:09:28 EST 2012


This is cool work and relevant to a lot of people in the PRL.  -- David


-------- Original Message --------
Subject: [MIT-PL] TALK:Tuesday 11-13-12 PL/SE Seminar: HALO: Haskell to 
Logic through Denotational Semantics
Date: Mon, 05 Nov 2012 17:01:02 -0500
From: Csail Event Calendar <eventcalendar at csail.mit.edu>
To: pl at csail.mit.edu


PL/SE Seminar: HALO: Haskell to Logic through Denotational Semantics
Speaker: Dimitrios Vytiniotis
Speaker Affiliation: Microsoft Research
Host: Adam Chlipala
Host Affiliation: CSAIL

Date: 11-13-2012
Time: 2:00 PM - 3:30 PM
Location: 32-G449 (Patil/Kiva)

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.

Joint work with Koen Claessen, Simon Peyton Jones, and Dan Rosen

Relevant URL(S): http://research.microsoft.com/en-us/people/dimitris/
For more information please contact: Adam Chlipala, adamc at csail.mit.edu

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl





More information about the PRL mailing list