During Ferienakademie 2024,
a team of roughly 15 students, myself included, worked on OshrEQ, a VSCode extension for functional
programming and verification that
automatically checks proofs written in MiniOCaml, a simplified subset of the OCaml language.
While I contributed to the original version developed during the two-week period of the academy,
I did not contribute to the paper or any further modifications to the project in any way¹, so I
won't claim any ownership of that. This page merely exists for archival purposes. This is
why you'll have to visit one of the two links to access the paper or cite it - I don't want to
take anything away from that.
Nevertheless, below is the publicly available abstract of the conference paper made for SKILL 2025, alongside links to
the ResearchGate page of the paper² and the GitHub
repository.
Equational reasoning in combination with induction is a powerful technique to prove equivalence of two
programs, and is therefore often taught in introductory courses on functional programming and
verification. In this paper, we present OshrEQ, a proof assistant for such kinds of proofs. OshrEQ takes
MiniOCaml, a core functional subset of the programming language OCaml, as input and enables students to
interactively construct proofs that are automatically checked for correctness. The equational part is
based on a set of rules, including variable renaming, substitution and pattern matching. New rules can
be added as lemmas and used in subsequent proofs. An existing SMT solver
is used to validate arithmetic and logical rewriting. The user-friendly interface and real-time feedback
to students is realized by means of a Visual Studio Code extension.
¹: Except for the unofficial logo I made to serve as the button icon for this page.
²: Though it's easier to access the paper directly under the GitHub release page.
