|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 listsCGC Advanced Technology Lectures Law Related Talks at Hughes Hall Institute of Theoretical Geophysics Informal Lunchtime Seminars (DAMTP)
Other talksRoles of cytoskeleton in hippocampal synaptic plasticity The Quantum Measurement Problem The genetic epidemiology of prostate cancer Running Out of Energy? The Future of the UK’s Electricity Supply. Epigenetic pathways in transcription and cancer Stem cells in lung maintenance and repair