|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 listsCivil Engineering Talks Whiston Society Data Insights Cambridge
Other talksIt’s not MPC! An Explicit Reference Governor for the supervision of constrained nonlinear systems The 2016 Alzheimer's Disease Congress Rare Metabolic Disorders: detection, research, management and treatment Imaging organic aerosols Immigrant Access in the Affordable Care Act: Legacies of the Confederacy Woofing it down – lessons on the neurobiology of appetite from man’s best friend