01
Research internship
Aristarchus
A verifier for the Hypatia proof language
Aristarchus is the verifier at the core of Hypatia: a Metamath-style proof checker that validates formal derivations rather than searching for proofs. It reads a Hypatia document, builds its syntax tree from a source whose syntax is context-dependent, and checks it against the rules of the language — returning either a clean pass or a structured tree of diagnostics that mirrors the structure of the source.
It is written in Haskell and uses applicative, error-accumulating validation, so a single run reports as many problems as it can. I work on it as part of a research internship under the supervision of Prof. Fabio Mogavero, and it is the subject of my Bachelor’s thesis.
-- Errors accumulate instead of short-circuiting:
-- one run reports every problem, not just the first.
data Result e a
= Failure [e]
| Success a
instance Applicative (Result e) where
pure = Success
Success f <*> Success x = Success (f x)
Failure e1 <*> Failure e2 = Failure (e1 ++ e2)
Failure e1 <*> Success _ = Failure e1
Success _ <*> Failure e2 = Failure e2