# 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

**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

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

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