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 Aug Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00: Paper Session 2: VerificationHaskell at Aurora Borealis Chair(s): Ningning XieThe University of Hong Kong | |||
13:30 - 14:00 Research paper | Verifying Effectful Haskell Programs in Coq Haskell Jan ChristiansenFlensburg University of Applied Sciences, Germany, Sandra DylusUniversity of Kiel, Germany, Niels BunkenburgUniversity of Kiel, Germany | ||
14:00 - 14:30 Talk | Solving Haskell equality constraints using Coq Haskell File Attached | ||
14:30 - 15:00 Experience report | Formal Verification of Spacecraft Control Programs: An Experience Report Haskell Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Jakob LechnerRUAG Space Austria GmbH |