Scholarlink

We report on a machine supported verification of a sorting algorithm from Haskell’s GHC library based on Natural Mergesort. Our work was motivated by previous endeavors with the Dafny system and with Isabelle/HOL, where a skillful elimination of mutual recursion is required to enable verification. We replicate the Isabelle/HOL solution with the VeriFun system and also give a direct proof for verifying correctness and stability of GHC-Mergesort. Based on our experiences when working on the proofs, we suggest a simpler implementation of Natural Mergesort. We conclude by comparing the degree of machine support of the considered systems when creating the proofs.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Largely Automated Verification of GHC’s Natural Mergesort

  • 章节

  • 发表日期：

    2025年

查看全文
  • Christoph Walther

摘要

We report on a machine supported verification of a sorting algorithm from Haskell’s GHC library based on Natural Mergesort. Our work was motivated by previous endeavors with the Dafny system and with Isabelle/HOL, where a skillful elimination of mutual recursion is required to enable verification. We replicate the Isabelle/HOL solution with the VeriFun system and also give a direct proof for verifying correctness and stability of GHC-Mergesort. Based on our experiences when working on the proofs, we suggest a simpler implementation of Natural Mergesort. We conclude by comparing the degree of machine support of the considered systems when creating the proofs.