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

[Matthias Felleisen]

Carl's defense conflicts with this talk. 


On Nov 5, 2012, at 6:09 PM, David Van Horn wrote:

> 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
> 
> 
> 
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4373 bytes
Desc: not available
Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20121105/2a56ebdf/attachment.bin