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
- Amy Felty and Brigitte Pientka. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison (draft). (pdf, appendix), to appear at ITP'10.
- Brigitte Pientka and Joshua Dunfield. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). To appear at IJCAR'10. (abstract) (pdf)
- Brigitte Pientka. Beluga: programming with dependent types, contextual data, and contexts (Invited talk). In 10th International Symposium on Functional and Logic Programming (FLOPS'10), Lecture Notes in Computer Science (LNCS), Springer, April 2010. (abstract) (pdf)
- 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.
Questions and bugs: Send email to Brigitte Pientka (bpientka at cs.mcgill.ca)
Current implementation:
- Version 0.2 (22 Jan. 2010) (includes an interpreter; supports context subsumption)
- An Emacs mode for Beluga (written by Stefan Monnier) is part of the distribution.
- Tutorial
- Grammar
Older versions:
- 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 Sept. 2009)
Tutorial:
The tutorial discusses five case studies done in Beluga. All of them revolve around the simply-typed lambda-calculus, and demonstrate the differences from other systems supporting HOAS.
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:
- Brigitte Pientka
- Stefan Monnier
- Joshua Dunfield (postdoc)
- Renaud Germain (Masters student)
- Ali Assaf (undergraduate student)