To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

HALO: Haskell to logic th… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

HALO: Haskell to logic through denotational semantics

Conference paper
Authors Dimitrios Vytiniotis
Simon L. Peyton-Jones
Dan Rosén
Koen Claessen
Published in Conference Record of the Annual ACM Symposium on Principles of Programming Languages
Pages 431-442
ISBN 978-1-4503-1832-7
ISSN 0730-8566
Publication year 2013
Published at
Pages 431-442
Language en
Keywords first-order logic, static contract checking
Subject categories Software Engineering


Even well-typed programs can go wrong in modern functional languages, by encountering a pattern-match failure, or simply returning the wrong answer. An increasingly-popular response is to allow programmers to write contracts that express semantic properties, such as crash-freedom or 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 an off-the-shelf first-order logic theorem prover.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?