|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 listsTwentieth Century Think Tank Genetics Department Seminar Series Quantitative cell biology symposium: June 18 2009
Other talksEXPRESSION OF FIBROBLAST ACTIVATING PROTEIN (FAP) IN TUMOUR ASSOCIATED FIBROBLASTS (TAF) OF CANINE MAST CELL TUMOURS AND CORRELATION WITH TMOUR GRADE AND MITOTIC INDEX Lunchtime Seminar with CAPREX fellows from Makerere University, Uganda Biobanking 2016 Parabolic and Hyperbolic Unimodular maps The evolution of Business Models [Provisional - TBC] Filming Fore, shooting scientists: medical research and documentary film