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
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00: Haskell 2019 - Paper Session 2: Verification at Aurora Borealis
Chair(s): Ningning XieThe University of Hong Kong
haskellsymp-2019-papers13:30 - 14:00
Research paper
Jan ChristiansenFlensburg University of Applied Sciences, Germany, Sandra DylusUniversity of Kiel, Germany, Niels BunkenburgUniversity of Kiel, Germany
haskellsymp-2019-papers14:00 - 14:30
File Attached
haskellsymp-2019-papers14:30 - 15:00
Experience report
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Jakob LechnerRUAG Space Austria GmbH