The metatheory of Standard ML was mechanized by Lee, Crary and Harper using Twelf. We set out to repeat this mechanization in order to assess the practicality and robustness of Beluga, a programming and proof environment with support for contextual types, using Harpoon, a more accessible frontend to Beluga.
Further developments for this mechnization have been moved to another repository.