Overview
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.
Tutorial:
- Mechanizing Meta-Theory in Beluga (CADE-25 Tutorial), August 2015
- Mechanizing Types and Programming Languages: A Companion: This is a companion that loosely follows B. Pierce's book "Types and Programming Languages"
and shows how to mechanize the material in Beluga. The code to the companion is available on
GitHub (see
beluga-code)
For an up-to-date version or to contribute see our GitHub repository.
Overview Talks:
- Mechanizing Meta-Theory in Beluga, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), June 2015
- 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)
Installation
Please refer to the installation guide in the GitHub repository of Beluga:
https://github.com/Beluga-lang/Beluga/blob/master/INSTALL.
Funding
This research has been funded through: NSERC (Natural Science and Engineering Research Council), FRQNT Recherche d'Équipe, 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 de l'Économie, de l'Innovation et de l'Énergie au Quebec.
© Computation and Logic Group 
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9