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

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.


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.


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.


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.