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.

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

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