package beluga

  1. Overview
  2. Docs
Implementation of contextual modal logic for reasoning with higher-order abstract syntax

Install

Dune Dependency

Authors

Maintainers

Sources

v1.0.tar.gz
md5=db38afa81edcccce71b1af2285283cef
sha512=7a0e7464233faa0f82026f2800fe105a1aade96abe88e4f9e62ac5e1a6b3b160240ced250b5bd16b86fcd48ece48d1e51cb94dcb4ac16d1fbc0dcd3f2b1a2ea1

README.md.html

Beluga

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.

Installation & Configuration Guide

The following packages must be installed to use Beluga:

Optional dependencies (for improved beli mode):

General instructions
$ YOUR_PKG_MNGR install opam
$ opam init --bare
$ opam switch create ocaml-base-compiler.4.09.0
$ eval $(opam env)
# from the Beluga directory
$ opam install --deps-only .

The interactive mode is greatly improved if you have rlwrap installed, so you might also want to consider:

$ YOUR_PKG_MNGR install rlwrap

Building

Compile by running "make" from the Beluga directory.

$ make

You can now run Beluga programs with the newly "beluga" executable in the "bin" directory

$ ./bin/beluga path/to/program.bel

Tip: Running make clean will clean the directory of compilation results

Interactive Mode

For interactive proofs, we recommend using Harpoon. A detailed list of commands and tactics is available here.

Beluga-mode for GNU Emacs

Beluga includes a major mode for programming in Emacs. The elisp file is located in the ./tools directory. To configure Beluga-mode:

  1. Update your ~/.emacs or ~/.emacs.d/init.el file with the lines written below. XEmacs users must update ~/.emacs or ~/.xemacs/init.el with the same text. Create any of these files if they do not exist already.

    • You should replace path/to/beluga with the actual path of the Beluga directory. (add-to-list 'load-path "path/to/beluga/tools/") (load "beluga-mode.el")

    • NOTE: Feel free to move the beluga-mode.el file to another directory so long as you add its location to the Emacs load-path.

  2. Restart Emacs. Emacs will now launch in Beluga-mode automatically when you open a Beluga program.

OCaml

Innovation. Community. Security.