Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Dmitrios Vytiniotis

LFCS Seminar: Dmitrios Vytiniotis

— filed under:

Static contract checking for Haskell through FOL semantics

  • LFCS Seminar
When Mar 20, 2012
from 04:00 PM to 05:00 PM
Where IF 4.31-33
Add event to calendar vCal

Any serious program contains assertions or documented function pre- and post-conditions. An alternative way to express such executable specifications is through contracts. In the context of Haskell, contracts have a well-defined operational semantics, but previous work does not settle the subject of statically checking contracts, expressed as ordinary programs, in an effective and practical way for a lazy functional language. In this work (in progress) we aim to address the problem taking a denotational semantics approach: We express the semantics of programs and of contracts directly in terms of first-order logic formulae and automatically discharge the proof obligations that arise using a first-order logic theorem prover. We show how we leverage the purity of Haskell for equational reasoning, how we use information from counter-models, how to avoid the search space explosion in the theorem prover, and how induction can possibly work. I will also demonstrate our ideas with a demo of our prototype implementation and sketch extensions to other features of the Haskell language, such as type classes.

Document Actions