BibTeX

@inProceedings{vytiniotis-etal-2013-halo-187462,
	title        = {HALO: Haskell to logic through denotational semantics},
	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.},
	booktitle    = {Conference Record of the Annual ACM Symposium on Principles of Programming Languages},
	author       = {Vytiniotis, Dimitrios and Peyton-Jones, Simon L. and Rosén, Dan and Claessen, Koen},
	year         = {2013},
	ISBN         = {978-1-4503-1832-7},
	pages        = {431--442},
}

@article{vytiniotis-etal-2013-halo-178613,
	title        = {HALO: Haskell to Logic through Denotational Semantics},
	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. },
	journal      = {Acm Sigplan Notices},
	author       = {Vytiniotis, D. and Jones, S. P. and Rosén, Dan and Claessen, Koen},
	year         = {2013},
	volume       = {48},
	number       = {1},
	pages        = {431--442},
}

@inProceedings{claessen-etal-2013-automating-175485,
	title        = {Automating Inductive Proofs using Theory Exploration},
	abstract     = {HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational  properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.},
	booktitle    = {24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013},
	author       = {Claessen, Koen and Rosén, Dan and Johansson, Moa and Smallbone, Nicholas},
	year         = {2013},
	volume       = {7898},
	ISBN         = {978-3-642-38573-5},
	pages        = {392--406},
}