Typing a simple programming language (again)

Samuel Mimram

This TD is optional, only do it if you have finished the previous ones.

We are now going to do again the first TD, but in Agda this time, and showing that our language has the expected properties.

1 Definition of the programming language

We consider the simple programming language presented in the course where an expression p consists of either

1.1 A type for programs

Define a recursive type Prog which implements programs.

1.2 Deciding inequality of natural numbers

Show that the relation \(<\) on natural numbers is decidable.

1.3 Reduction

We recall that the rules for reduction of programs are

reduction rules

Define the reduction relation:

__ : Prog  Prog  Set

1.4 Types

Define a type Type of types for our language.

1.5 Typing

Define the typing relation for the language:

__ : Prog  Type  Set

2 Properties

2.1 Subject reduction

Show the subject reduction property: if a program \(p\) has type \(A\) and \(p\) reduces to \(p'\) then \(p'\) also has type \(A\).

2.2 Progress

Show the progress property: a typed program either is a value (a natural number or a boolean) or reduces.

3 Extensions

3.1 Products

Add products to the language.

3.2 Unit

Add a units to the language.

3.3 Abstractions

Add λ-abstractions to the language (this is hard!).