Just FYI, "Beluga" also refers to a proof assistant based on the logical framework with contextual modal type theory: http://complogic.cs.mcgill.ca/beluga/