# Beluga

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.

- Beluga webite: Informaion on downloading Beluga, Tutorial, etc.
- Twelf Wiki: For a tutorial on using the logical framework to specify formal systems.

- Beluga:programming with dependent types, contextual data, and contexts,Invited talk). In 10th International Symposium on Functional and Logic Programming (FLOPS'10), Lecture Notes in Computer Science (LNCS), Springer, April 2010.
- ,Programming inductive proofs: a new approach based on contextual types,, Brigitte Pientka, Verification, Induction, and Termination analysis, LNAI, Springer, Aug 2010
- Logical frameworks, Frank Pfenning. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 17, pages 1063-1147. Elsevier Science and MIT Press, 2001

# Related systems:

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

- Twelf system: it provides an implementation of the logical framework LF. It supports the specification of formal systems given via axioms and inference rules and many such specifications can be executed by a higher-order logic programming engine. Proofs about formal systems are implemented as relations and Twelf provides various checkers to guaranteed that these relations are total functions.

The strength and elegance of LF comes from supporting encodings based on higher-order abstract syntax (HOAS), in which binders in the object language are represented as binders in LF's meta-language. As a consequence, users can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution, renaming and fresh name generation. Because of this, one can think of HOAS encodings as the most advanced technology for specifying and prototyping formal systems which leads to very concise and elegant encodings and provides the most support for such an endeavor. - Agda2: it is a dependently typed functional programming language based on Martin-Löf type theory. At the same time, Agda is a proof assistant. It is an interactive system for writing and checking proofs. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL. Because of the strong theoretical foundation these systems are built on, they cannot support encodings using higher-order abstract syntax. As a consequence, different approaches to encoding formal systems together with their meta-theory are developed which typically increase the burden on the user to manage and prove bureaucratic details about bound variables and assumptions.
- TBA

# Emacs

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.