Beluga supports the specification of formal systems given by axioms and inference rules within the logical framework LF. It also supports implementing proofs about formal systems as dependently typed recursive functions. What distinguishes Beluga from other frameworks is that it not only represents binders using higher-order abstract syntax, but directly supports reasoning with contexts and contextual objects. Contextual types allows us to characterize precisely hypothetical and parametric derivations, i.e. derivations which depend on variables and assumptions, and lead to a direct and elegant implementation of inductive proofs as recursive functions. Because of the intrinsic support for binders and contexts, one can think of the design of Beluga as the most advanced technology for specifying and prototyping formal systems together with their meta-theory.


Related systems:

There are many related systems and we only mention a few approaches which are most relevant to this course.


Emacs (available in two implementations, GNU Emacs and XEmacs) is a powerful and widely used family of text editors. It is well-suited for Beluga development, since it is highly customizable and extensible, and there exists a package for emacs called beluga-mode, which comes with the Beluga distribution. See the FAQ page for more detailed information on obtaining, installing, and using emacs.