Downloads

• Clone the latest version of Beluga from GitHub: https://github.com/Beluga-lang/Beluga.git.

Older versions:

• Version 1.1.1 (11 September 2023) Add support for fixity pragmas before delcarations.
• Version 1.1 (4 August 2023) Add an automated proof search tactic for Harpoon, and rework parsing and identifier resolution.
• Version 1.0 (18 March 2021) Introduce the Harpoon interactive proof environment.
• Version 0.8.2 (24 July 2015) Supports substitution variables, totality checking, and interactive proof development via holes and automatic splitting. It supports using explicit substitution attached to meta-variables.
• Version 0.8.1 (10 March 2015) Substitution variables, totality checking, and interactive proof development via holes and automatic splitting.
• Version 0.7 (2 June 2014) Introduction of turnstile, extension of substitution variables.
• Version 0.6 (13 February 2014)
• Version 0.5 (7 Feb 2013) Beluga development supporting indexed recursive types.
• Version 0.5 (20 Sep 2012) computation-level inductive datatypes, extended coverage checking, logic engine, revised syntax, revised error messages.
• Version 0.3 (7 Oct 2010) revised coverage checking and improved error messages, emacs mode
• Version 0.3 (4 Sep 2010) revised coverage checking (experimental) and includes bug fixes
• Version 0.3 (30 Aug 2010) supports context reconstruction, coverage checking and writing absurd patterns (experimental)
• Version 0.3 (7 Jul 2010) supports context reconstruction and coverage checking (experimental)
• Version 0.2 (22 Jan 2010)
• Version 0.1 (15 Dec 2009) (compiles under OCaml 3.10 and 3.11; supports context subsumption)
• Version 0.1 (16 Oct 2009)
• Version 0.1 (25 Sep 2009)

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9