ICFP 2020 (series) / HIW 2020 (series) / HIW 2020 /
Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
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
Fri 28 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
14:00 - 14:22 Talk | Implementation of linear types HIW | ||
14:22 - 14:44 Talk | Circuit Notation Source Plugin HIW Christopher ChalmersMyrtle.ai | ||
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 |