# 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}.

Update (06 September, 2012): We did an overhaul of the syntax of Beluga. Please refer the grammar description and the beginners guide for details.

### 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.

```datatype tp : type =
| arr : tp → tp →  tp
| nat : tp
;
%name tp T.

datatype exp : type =
| lam : tp  → (exp → exp) → exp
| app : exp → exp → exp
;
%name exp E.
```

### Examples

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

• λ x:nat.x is represented as lam nat \x.x.
• λ x:nat ⇒ nat. λ y:nat. x y is represented as lam (arr nat nat) (\x. lam nat \y. app x y).

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

Next, we define the typing judgment.

```datatype type_of : exp → tp → type =
| 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
;
%name type_of H.
```

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)..