|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Halo: From Haskell to Logic through Denotational Semantics
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:
Note that ex-directory lists are not shown.
Other listsCUSAS Forum Speaker Series Silicon Valley comes to the UK 2011 Finance & Accounting Seminar Series
Other talksSCISOC TALK: ATP-sensitive potassium channels and neonatal diabetes – from molecule to new therapy and beyond. 'Addressing the Spirit of Discernment: Pentecostal transformation of demonic objects into modern heritage in Sierra Leone Eating and drinking as a medieval peasant. Innovations in table manners in late medieval rural Valencia Detection of climate and environmental change in the big data era Session 7 - Sites for science and their heritage ATP-sensitive K channels and Neonatal Diabetes - from Molecule to New Therapy and Beyond