[TYPES] Release of Beluga prototype

[Brigitte Pientka]

Dear all,

 we'd like to announce the first release of Beluga.

The Beluga implementation provides an implementation of the logical
framework LF, and in addition a functional programming environment
which supports dependent types and analyzing LF data via pattern
matching. It is a completely new implementation effort. Its
implementation of the logical framework LF in OCaml shares, adapts and
extends some fundamental ideas from the Twelf system. The functional
programming environment which is built on top of the logical framework
LF is a completely new implementation based on previous theoretical
ideas presented in [Pientka:POPL08] and [PientkaDunfield:PPDP08].

At this point our prototype supports type reconstruction for LF
signatures as well as type reconstruction for dependently typed
functional programs over LF data.

To get a feel for Beluga, you can download our prototype together with
examples and the papers describing the foundation from

 http://complogic.cs.mcgill.ca/beluga/

Comments, questions, and bugs should be sent to
beluga-dev at cs.mcgill.ca.

Best,

 Beluga-Developers

(Joshua Dunfield, Renaud Germain,
 Stefan Monnier, Brigitte Pientka)