A functional language for reasoning about formal systems, with higher-order abstract syntax and contexts as first-class objects.
LF tm : type =
| lam : (tm → tm) → tm
| app : tm → tm → tm;
schema ctx = tm;
% bind each free variable under a λ
rec close : {g:ctx} [g ⊢ tm] → [ ⊢ tm] =
mlam g ⇒ fn t ⇒ case t of
| [ ⊢ _] ⇒ t
| [g', x:tm ⊢ T] ⇒
close [g'] [g' ⊢ lam \u. T];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.
Install
Beluga ships as an opam package for Linux, WSL (Windows Subsystem for Linux), and macOS.
Quickstart
Install opam, then initialize it:
opam init
eval $(opam env)Install Beluga and refresh your shell environment:
opam install beluga
eval $(opam env)
You should now have beluga and harpoon in
$OPAM_SWITCH_PREFIX/bin.
Check a file or start Harpoon:
beluga path/to/program.bel
harpoon --sig path/to/program.belClick below if you run into any issues.
Full install guide
Prerequisites
The published package needs OCaml ≥ 4.14; opam pulls the rest. Optional: rlwrap for nicer interactive sessions. Building from source also needs GNU Make 4.0+.
After opam init, accept shell-hook setup if offered so new terminals
pick up opam automatically. Otherwise run eval $(opam env) in every
shell before calling beluga or harpoon.
Installing opam
Debian / Ubuntu (and Ubuntu under WSL):
sudo apt-get update
sudo apt-get install opam
# optional
sudo apt-get install rlwrapmacOS (via Homebrew):
brew install opam
# optional
brew install rlwrapWSL: install WSL, open your Linux distribution, then follow the Debian/Ubuntu steps.
Dedicated opam switch
If opam install beluga hits dependency conflicts in a shared switch, use an
empty local switch:
mkdir beluga-switch && cd beluga-switch
opam switch create . --empty
opam install beluga
eval $(opam env)Uninstall with opam remove beluga.
Install from source
For the development tip instead of the last opam release. Requires Git and GNU Make:
git clone https://github.com/Beluga-lang/Beluga.git Beluga
cd Beluga
make setup-install
make install
eval $(opam env --switch=. --set-switch)Uninstall with make uninstall from the clone.
Contributors who want tests and docs tooling should use
make setup-development instead — see the
repository README
(make, make test, dune exec …).
Emacs mode
Major mode in the repo’s
tools/
directory. Add to ~/.emacs or ~/.emacs.d/init.el
(replace path/to/beluga):
(add-to-list 'load-path "path/to/beluga/tools/")
(load "beluga-mode.el")
Restart Emacs. Ensure beluga / harpoon are on the PATH Emacs
sees (same eval $(opam env) environment as your shell).
Troubleshooting
Command not found after install — run eval $(opam env) again
(or eval $(opam env --switch=. --set-switch) inside a source clone).
Inconsistent interface assumptions after a partial build:
make clean
make install Failed install on windows? Use WSL instead. Currently Beluga depends upon linenoise,
which has POSIX headers, and so opam install beluga will not complete.
Docs
All publications- Beluga reference guide
-
Beginner's Guide to Programming in Beluga
This guide is mostly for users who have only a background in functional programming as often taught in an undergraduate class. We show how to write some common simple functional programs in Beluga and also briefly discuss how to write simple proofs.
Programs from the guide- nat.bel naturals §2
- yn.bel yes and no §2
- listnat.bel lists of naturals §2
- dtlist.bel length indexed lists §3
- typesterms2.bel list filtering §3
- typesterms3.bel list filtering §3
- typesterms.bel evaluation is deterministic §4
- lambda.bel preservation for the lambda-calculus §5
- Beluga: Programming Proofs About Formal Systems
- Mechanizing Meta-Theory in Beluga
-
Mechanizing Types and Programming Languages: A Companion
A companion that loosely follows B. Pierce's Types and Programming Languages and shows how to mechanize the material in Beluga. The code to the companion is on github (see beluga-code). For an up-to-date version, or to contribute, see our github repository.
- Mechanizing Meta-Theory in Beluga
- Programming logical relations proofs
- Beluga-mu: Programming proofs in context
- Beluga-mu: Programming proofs in context
Case studies
Close Terms
We build a simple program that closes open terms, converting each free variable to one bound by a lambda abstraction. The example demonstrates pattern matching on contexts and Beluga's built-in mechanism for variable substitution.
Type Uniqueness
Since Beluga does not support equality types, we implement equality using an LF type family as a dependent kind. The difficulties of defining equality via reflexivity in Twelf do not arise in Beluga. Beluga's proof is implemented as a function using pattern matching instead of relations; as we pattern match we learn more about the given derivations and information flows as expected.
Parallel Reduction
The order of assumptions in a context is important in Beluga. However, sometimes the need to reorder assumptions arises, as is illustrated in the proof of the substitution lemma for algorithmic equality. As in Twelf this kind of proof does not come for free in Beluga.
Polymorphic Algorithmic Equality
In order to prove algorithmic equality for a polymorphic lambda-calculus, we establish schemas with alternating assumptions, depending on the type of the variable.
Poplmark
This example shows a solution of the POPLMARK Challenge Part 1A, Transitivity of Subtyping.
Untyped Algorithmic Equality — Context Relation
Context relationships can be defined explicitly using inductive datatypes. In this proof we use inductive datatypes to establish strengthening and weakening between contexts.
Untyped Algorithmic Equality — Context Subsumption
This example demonstrates Beluga's capacity for automatic context subsumption. If schema W is a prefix of a schema W0, then we can always use a context of schema W0 in place of a context of schema W.
Normalization by Evaluation
A normalization by evaluation algorithm for an intrinsically typed simply-typed lambda calculus.
Weak Normalization
A proof of weak head normalization for the simply typed lambda calculus using logical relations.
People
McGill's Computation and Logic (Complogic) Group is the team behind Beluga, focused on developing a theoretical and practical foundation for building and reasoning about software systems. Research areas include logic and programming languages, type theory, logical frameworks and software verification.