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.

Overview Installation Documentation


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.


Overview Talks:


This research has been funded through: NSERC (Natural Science and Engineering Research Council), FQRNT Recherche d'Equipe, PSR-SIIRI Projets conjoints de recherche et d'innovation and 63e session de la Commission permanente de coopération franco-québécoise by Ministère du Développement économique, de l'Innovation et de l'Exportation au Quebec,