|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 listsPhilosophy of Physics Engineering Department Computing Seminars Wellcome Lecture in the History of Medicine
Other talks日本語母国語話者による英語発音の通じやすさと印象 The Plurality of Worlds The Uniates and the Invention of Eastern Orthodoxy Late Byzantine and early Ukrainian Advocates of Church Union in the Crossfire between Rome, Constantinople, and Moscow Peter Latham (Department for Transport) Title: First do no harm Artificial Intelligence: Disrupting Sustainability; “Looking towards 2050”