Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Fri 28 Aug 2020 15:45 - 15:57 at HIW - Sessions 4 and 5

If a codebase is so big and complicated that complete mechanical verification is intractable, can we still benefit from verification methods? We show that by constructing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.

Fri 28 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 17:30: Sessions 4 and 5HIW at HIW
14:00 - 14:22
Talk
Implementation of linear types
HIW
14:22 - 14:44
Talk
Circuit Notation Source Plugin
HIW
15:00 - 15:45
Talk
Lightning Talks 2
HIW
15:45 - 15:57
Talk
Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
HIW
Antal Spector-ZabuskyUniversity of Pennsylvania, Joachim BreitnerDFINITY Foundation, Stephanie WeirichUniversity of Pennsylvania, Yao LiUniversity of Pennsylvania
16:00 - 16:20
Talk
Closing
HIW
Ben GamariWell-Typed LLP