Beluga is a functional programming language designed for reasoning about formal systems. It features direct support for object-level binding constructs using higher order abstract syntax and treats contexts as first class objects.
Beluga allows specification of formal systems (such as lambda calculi and type systems) using a foundation of contextual modal logic. As in the Twelf system, we can encode object-level binding constructs using higher order abstract syntax. We also pair terms with the contexts that give them meaning and then reason about these contextual objects. Proofs in Beluga are represented by recursive programs according to the Curry-Howard Isomorphism.
Beluga is developed at the Complogic group at McGill University, led by Professor Brigitte Pientka. It is implemented in OCaml.
To learn more about Beluga we recommend the following tutorial style papers and talks. If you have trouble discerning Beluga code from older releases, consult the legacy syntax for clarification.
- Beluga: programming with dependent types, contextual data, and
contexts, Brigitte Pientka, Invited talk at 10th
International Symposium on Functional and Logic Programming
(FLOPS'10), April 2010, Sendai, Japan.
- Programming inductive proofs: a new approach based on contextual
types, Brigitte Pientka, Verification, Induction, and Termination analysis, LNAI, Springer, Aug 2010
- Programming logical relations proofs, Brigitte Pientka, Certification of high-level and low-level programs, Institut Henri Poincare, Paris, France, June 2014 (slides)
- Beluga-mu: Programming proofs in context, Brigitte Pientka, POP Seminar, Carnegie Mellon University, May 2014 (slides)
- Beluga-mu: Programming proofs in context, Brigitte Pientka, Invited talk at International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'12). (slides)
- Install all the prerequisite packages.
- Download the Beluga source code.
- From the Beluga directory, build the executable by using:
- Use the executable located in the bin directory to run Beluga programs:
~/beluga# bin/beluga path/to/program.belto run a Beluga program.
- Run in an Emacs buffer to use the Interactive mode. See the Docs file for how to use the Interactive mode commands.
BugsFor any bugs or issues please send an email to