|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 listsAutomating Biology using Robot Scientists Geometry, Integrability and Twistor Theory Institution of Civil Engineers (Cambridge Branch)
Other talksLunchtime Talks As if by Magic...... Spectacular Chemistry Demonstration Lecture TBC Politics in Common in the Digital Age Senescence, cell death and apoptosis Neutrophil transmigration in vivo: Mechanisms, dynamics and pathogenesis