Halo: From Haskell to Logic through Denotational Semantics

Add to your list(s) Download to your calendar using vCal

• Dimitrios Vytiniotis, MSR Cambridge
• Friday 23 November 2012, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Bjarki Holm.

Even well-typed programs can go wrong, by encountering a pattern-match failure, or simply returning the wrong answer. And increasingly-popular response is to allow programmers to write contracts that express behavioural properties, such as crash-freedome of 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 off-the-shelf first-order theorem provers.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Computing and Mathematics
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology

Note that ex-directory lists are not shown.