[TYPES/announce] Beluga release: programming with proofs

[Brigitte Pientka]

Dear all,

 we'd like to announce the second release of Belgua.

 Beluga is a dependently-typed programming and proof development
environment which uses a two-level approach: it supports specifying
formal systems within the logical framework LF and on top of LF, it
provides a dependently-typed functional language that supports
manipulating and analyzing contextual LF objects (i.e. LF objects in
context) via pattern matching. Most recently, we added indexed
recursive types drawn from contextual LF.

The implementation is based on previous theoretical ideas presented in
[Pientka:POPL08], [PientkaDunfield:PPDP08], and [CavePientka:POPL12].

Recent additions to Beluga are

- Indexed recursive types as described in [CavePientka:POPL12]
- Revised uniform source syntax for declaring LF types. indexed
recursive types, and contextual objects
- Pattern matching on contexts and contextual objects
- Basic support to program with holes in programs
- Type definitions
- Coverage checking for contextual LF objects
- A logic programming interpreter for LF
- More robust error handling
- Interactive interpreter for Beluga

Our examples include

- PROOFS: such as Church-Rosser, Cut-elimination, mechanized
development of Ch 3, Ch 6, and Ch 14 from "Types and Programming Languages"  by
B. Pierce.

- PROGRAMS: Normalization by evaluation, Translating between HOAS and deBruijn
  representation, Closure conversion, Certifying type checker

To get a feel for Belgua, you can download our recent prototype together with
many examples from

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

Comments, questions, and bugs should be directed to beluga-developers
mailing list. You can subscribe to it at:

 http://mailman.cs.mcgill.ca/mailman/listinfo/beluga-dev

Best,

 Beluga-Developers

Brigitte Pientka,  Mathieu Boespflug, Costin Badescu, Olivier Savary
Belanger, Stefan Monnier