package beluga

  1. Overview
  2. Docs
On This Page
  1. Private Libraries
Implementation of contextual modal logic for reasoning with higher-order abstract syntax

Install 

dune-project
 Dependency

complogic.cs.mcgill.ca Readme Changelog Edit opam file Versions (7)

Authors

  1. B
    Brigitte Pientka
  2. J
    Joshua Dunfield
  3. A
    Andrew Cave
  4. J
    Jacob Thomas Errington
  5. J
    Junyoung Clare Jang
  6. M
    Marc-Antoine Ouimet

Maintainers

  1. M
    marc-antoine.ouimet@mail.mcgill.ca

Sources

v1.1.3.tar.gz
md5=475d41b9d142441e966cfeab38aa1f60
sha512=dbdbe5233a120c5cac367cb3914f482c4d00e325786ee51f2c5892d7e5fdd556338ec9565106b9ad82e50b26c8dc235887bc9b2a75e5ad0e2f19fb95f642a8a9

doc/index.html

Beluga

At a surface level, the Beluga implementation produces two executables:

  1. The Beluga CLI
  2. The Harpoon CLI

The Beluga CLI includes a legacy interactive mode interpreter. This is used by the replay executable to interactively test some of the functionalities of the core Beluga system. This interactive system is mostly superseded by Harpoon.

Private Libraries

The Beluga system is comprised of multiple private libraries. These are listed below in topological order of dependency.

  • Support is the library of miscellaneous utility functions, data structures, and extensions to imported libraries.
  • Optparser is a library for parsing CLI arguments using combinators.
  • Beluga_syntax is the library defining the data types for the various syntaxes and common syntactic elements of Beluga and Harpoon.
  • Beluga_parser is the library for parsing Beluga signatures and Harpoon commands.
  • Beluga_html is a library for pretty-printing external Beluga signatures to HTML.
  • Beluga is the core library of Beluga, which deals with signature reconstruction, type-checking, coverage-checking and termination-checking. It also features modules handling the legacy interactive mode for Beluga, as well as proof search using logic programming.
  • Harpoon is the new interactive frontend to Beluga.