A type-preserving compiler in Haskell

There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants in order to capture in the types important invariants of the program. This allows type-based program verification and is a promising compromise between plain old types and full blown Hoare logic proofs.

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Louis-Julien Guillemette, Stefan Monnier
• Keywords: Hoare Logic Proofs, ICFP 2008, Programming Languages, Type-based Program Verification, Types Important Invariants