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
- Olivier Savary-Belanger, Stefan Monnier and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax, 3rd International Conference on Certified Programs and Proofs (CPP'13). (code)
- Brigitte Pientka. Coverage checking contextual objects, submitted June 2012, (tar-ball with Beluga examples)
- Andrew Cave and Brigitte Pientka. Programming with Binders and Indexed Data-types, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12).
- Mathieu Boespflug and Brigitte Pientka. Multi-level Contextual Type Theory, 6th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'11) (long version).
- Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records, 10th Conference on Typed Lambda Calculi and Applications (TLCA'11). (long version)
- Brigitte Pientka and Joshua Dunfield. Covering all bases: design and implementation of case analysis for contextual objects. Technical report, Oct 2010. (pdf, electronic appendix, electronic appendix (tar-ball))
- Amy Felty and Brigitte Pientka. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. In First International Conference on Interactive Theorem Proving (ITP'10), Lecture Notes in Computer Science (LNCS), vol 6172, page 227-242, Springer, 2010. (abstract) (pdf) (appendix)
- Brigitte Pientka and Joshua Dunfield. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In 5th International Joint Conference on Automated Reasoning (IJCAR'10), Lecture Notes in Computer Science (LNCS), vol 6173, page 15-21, Springer, 2010. (abstract) (pdf)
- Andreas Abel and Brigitte Pientka. Explicit substitutions for contextual type theory. In 5th International Workshop on Logical Frameworks: Theory and Practice (LFMTP'10), Electronic Proceedings in Theoretical Computer Science (EPCS), vol 34, page 5 - 21, 2010. (electronic version of proceeding) (abstract) (pdf) (Implementation of type-checker in Haskell)
- Brigitte Pientka. Programming inductive proofs: a new approach based on contextual types, Brigitte Pientka, Verification, Induction, and Termination analysis, Lecture Notes in Artificial Intelligence (LNAI), Springer, 2010
- 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), vol 6009, page 1-12, Springer, 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. 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:
- Version 0.5 (07 February 2013)
- An Emacs mode for Beluga (written by Stefan Monnier) is part of the distribution.
- A VIM plug-in for Beluga can be found here; contributed by Vincent Aravantinos.
- Grammar
Older versions:
- Version 0.5 (20 Sep 2012) computation-level inductive datatypes, extended coverage checking, logic engine, revised syntax, revised error messages.
- Version 0.3 (7 Oct 2010) revised coverage checking and improved error messages, emacs mode
- Version 0.3 (4 Sep 2010) revised coverage checking (experimental) and includes bug fixes
- Version 0.3 (30 August 2010) supports context reconstruction, coverage checking and writing absurd patterns (experimental)
- Version 0.3 (7 July 2010) supports context reconstruction and coverage checking (experimental)
- Version 0.2 (22 Jan. 2010)
- 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 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:
- nat.bel: naturals (Section 2);
- yn.bel yes and no (Section 2);
- listnat.bel: Lists of naturals (Section 2);
- dtlist.bel: length indexed lists (Section 3);
- typesterms2.bel: list filtering (Section 3);
- typesterms3.bel: list filtering (Section 3);
- typesterms.bel: evaluation is deterministic (Section 4);
- lambda.bel: lambda-calculus and proof of presevertation (Section 5).
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
- Mathieu Boespflug (postdoc)
- Francisco Ferreira (PhD student)
- Olivier Savary (Masters student)
- Costin Bǎdescu (undergraduate student)