Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 14:00 - 14:30 at Aurora Borealis - Paper Session 2: Verification Chair(s): Ningning Xie

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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning Xie University of Toronto
Research paper
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
File Attached
Experience report
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