While I don’t understand much algebra, I know Isabelle and implemented a checker in Isabelle/HOL. I used the Refinement Framework and Sepref to generated code in Standard ML. The code is mostly functional (except for the hashmap that is synthesized automatically by Sepref – no need to understand and know anything about it!). How does Pastèque work? I started with an abstract calculus that models the rules of the proofs system. Then I make the calculus more concrete, e.g., with lists to represent polynomials. Finally, I make everything executable. …

Pastèque 2 Pastèque 2 is available on the IsaFoL repository and the HTML generation can be seen too. The source code can be found here. Pastèque 1 Pastèque 1 is available with the Isabelle formalization on the Archive of Formal Proofs, where it is maintained and kept up-to-date. The release is also available here.