# Typing a simple programming language (again)

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

• b: a boolean
• n: an integer
• p + q: a sum of two expression
• p < q: a comparison of two expressions
• if p then q else r: a conditional branching

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

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 program either is a value (a natural number or a boolean) or reduces.