Solving Haskell equality constraints using Coq
The introduction of the Data Kinds and Type families GHC extensions has allowed a powerful technique for writing Haskell data structures which are Correct-by-Construction: GADTs indexed by Algebraic Data Types.
However, when defining operations on such data structures, there often arise type equalities that GHC is unable to prove. Furthermore, proving these equalities manually in Haskell is often a difficult or even impossible task.
Even when it is possible to write such proofs, they are usually “relevant” proofs, which must be executed at runtime. This is an unfortunate situation, as correctness should not come at the cost of speed.
This paper presents a typechecker plugin for GHC which can assert such equalities, while simultaneously translating their statements into Coq theorems, which can be proven and checked to ensure their correctness.
|Extended Abstract (main.pdf)||433KiB|
Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning Xie The University of Hong Kong
|Verifying Effectful Haskell Programs in Coq|
Jan Christiansen Flensburg University of Applied Sciences, Germany, Sandra Dylus University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany
|Solving Haskell equality constraints using Coq|
|Formal Verification of Spacecraft Control Programs: An Experience Report|
Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Jakob Lechner RUAG Space Austria GmbH