Sciweavers

POPL
2009
ACM

Static contract checking for Haskell

14 years 4 months ago
Static contract checking for Haskell
Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness. Categories and Subject Descriptors D.3 [Software]: Programming Languages General Terms verification, functional language Keywords contract satisfaction, static contract checking
Dana N. Xu, Simon L. Peyton Jones, Koen Claessen
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where POPL
Authors Dana N. Xu, Simon L. Peyton Jones, Koen Claessen
Comments (0)