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
Sitemap
To content Read more about how we use cookies on gu.se

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

Abstract

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
Share:

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?