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
- Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 163-173. ACM Press, July 2008. (abstract) (pdf) (bibtex)
- Joshua Dunfield and Brigitte Pientka. Case analysis of higher-order data. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08). Elsevier, June 2008. (abstract) (pdf—extended version including appendix) (bibtex)
- Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 371-382. ACM Press, January 2008. (abstract) (pdf) (bibtex)
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. The following people have contributed over the past year to the implementation: Joshua Dunfield, Renaud Germain, Stefan Monnier, and Darin Morrison.
Current implementation:
- Version 0.1 (16 Oct. 2009) (compiles under OCaml 3.10 and 3.11)
Older versions:
- Version 0.1 (25 Sept. 2009) (compiles under OCaml 3.10)
People:
- Brigitte Pientka
- Stefan Monnier
- Joshua Dunfield (postdoc)
- Renaud Germain (Masters student)
- Ali Assaf (Undergraduate student)