Beginner
Beginner's Guide to Programming in Beluga
This guide is mostly for users who have only a background in functional programming as often taught in an undergraduate class. We show how to write some common simple functional programs in Beluga and also briefly discuss how to write simple proofs in Beluga.Here are a few sample programs discussed in the tutorial to get you started
- 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 preservation (Section 5).
Close Terms
We build a simple program that closes open terms, converting each free variable to one bound by a lambda abstraction. The example demonstrates pattern matching on contexts and Beluga's built-in mechanism for variable substitution.
Type Uniqueness
Since Beluga does not support equality types, we implement equality using an LF type family as a dependent kind. The difficulties of defining equality via reflexivity in Twelf do not arise in Beluga. Beluga's proof is implemented as a function using pattern matching instead of relations; as we pattern match we learn more about the given derivations and information flows as expected.
Intermediate
Parallel Reduction
The order of assumptions in a context is important in Beluga. However, sometimes the need to reorder assumptions arises, as is illustrated in the proof of the substitution lemma for algorithmic equality. As in Twelf this kind of proof does not come for free in Beluga.
Polymorphic Algorithmic Equality
In order to prove algorithmic equality for a polymorphic lambda-calculus, we establish schemas with alternating assumptions, depending on the type of the variable.
Poplmark
This example shows a solution of the POPLMARK Challenge Part 1A, Transitivity of Subtyping.
Untyped Algorithmic Equality - Context Relation
Context relationships can be defined explicitly using inductive datatypes. In this proof we use inductive datatypes to establish strengthening and weakening between contexts.
Untyped Algorithmic Equality - Context Subsumption
This example demonstrates Beluga's capacity for automatic context subsumption. If schema W is a prefix of a schema W0, then we can always use a context of schema W0 in place of a context of schema W. Essentially, we allow the user to pass a context of schema W0 where a context with schema W if W0 contains at least as much information as W.
Advanced
Normalization by Evaluation
A normalization by evaluation algorithm for an intrinsically typed simply-typed lambda calculus.
Weak Normalization
A proof of weak head normalization for the simply typed lambda calculus using logical relations.
© Computation and Logic Group 
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9