Beluga: Functional Programming with Higher-Order Abstract Syntax

Our main interest in this project is to investigate programming and reasoning with data structures that provide support for binders. Many object languages include binding constructs, and it is striking that functional languages still lack direct support for binders and common tricky operations such as renaming, capture-avoiding substitution, and fresh name generation.

We advocate the use of higher-order abstract syntax (HOAS) where we represent binders in the object language with binders in the meta-language. One of the key benefits is that we not only get support for renaming and fresh name generation, but also for capture-avoiding substitution. While HOAS encodings have played an important role in mechanizing the meta-theory of programming languages, it has been difficult to incorporate HOAS encodings directly into functional programming.

Publications

Implementation

We are actively developing a prototype implementation of our language, Beluga, in OCaml. 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, 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].

The lead implementor is Brigitte Pientka. Since 2008, the following people have contributed to the implementation: Costin BĒŽdescu, Mathieu Boespflug, Andrew Cave, Joshua Dunfield, Francisco Ferreira, Renaud Germain, Stefan Monnier, Darin Morrison, Olivier Savary.

Questions and bugs: Send email to Brigitte Pientka (bpientka at cs.mcgill.ca)

Current implementation:

Older versions:

Tutorial

The tutorial offers a taste of what programming in Beluga is like, starting gently and working all the way up to proving type preservation for the simply typed lambda calculus. Here are the embedded code snippets as separate files, for easy loading into Beluga:

Benchmarks

Amy Felty and Brigitte Pientka proposed several benchmark problems which illustrate the differences and trade-offs in systems supporting programming and reasoning about higher-order abstract syntax encodings.In particular, we compare the development of these examples in the Twelf system, Beluga and Two-level Hybrid. See also Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison (draft).

People