Tutorial

We discuss five case studies done in Beluga. All of them revolve around the lambda-calculus. If you would like to run any of these examples, we suggest you download the files associated with each of the proofs instead of copy-pasting the code from the webpage. If you'd like to display the examples as we show them on these webpages, please use the emacs-mode for Beluga which is part of the Beluga distribution.

Update (20 April, 2010): We have recently added context reconstruction to Beluga. This means we can omit passing a context explicitely provided we omit the brackets and the star around a context schema declaration in a computation-level type, i.e. instead of writing {g:(ctx )*} we simply write {g:ctx}.

Defining the simply-typed lambda-calculus in LF

We begin by defining types and expressions in LF using higher-order abstract syntax. The main idea is to represent binders in the object-language (i.e., the on paper formulation of the lambda-calculus) with binders in our meta-language (i.e., LF). The constructor for abstractions hence takes in two arguments: the type of the input argument and a function of type (exp → exp) describing the body of the abstraction. For more information on how to represent formal systems in the logical framework LF see the excellent resources for the Twelf system. 

tp: type.                      %name tp T.
arr: tp → tp →  tp.
nat: tp.

exp: type.                     %name exp E.
lam : tp  → (exp → exp) → exp.
app : exp → exp → exp.

Examples

Next, we give a few examples of encoding lambda-terms from the object-language in our meta-language.

Defining the typing rules for the simply-typed lambda-calculus in LF

Next, we define the typing judgment.

type_of: exp → tp → type.     %name type_of H.

t_lam: ({x:exp}type_of x T1 → type_of (E x) T2)
	→ type_of (lam T1 E) (arr T1 T2).
	  
t_app: type_of E1 (arr T2 T) → type_of E2 T2
       → type_of (app E1 E2) T.

We again use ideas from higher-order abstract syntax representing the parameteric and hypothetical derivation in the premise of the typing rule for lambda-abstraction using a higher-order function with type ({x:exp}type_of x T1 → type_of (E x) T2). The definition t_lam reads as follows: if for all variables x assuming type_of x T1 implies type_of (E x) T2, then we can conclude type_of (lam T1 E) (arr T1 T2)..

Proofs about the simply-typed lambda-calculus

1. Type uniqueness

2. Reasoning about paths in lambda-terms

3. Subject reduction

4. Equality reasoning

5. Reasoning about smaller relation on lambda-terms