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

# 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

## A type for programs

Define a recursive type `Prog`

which implements programs.

## Deciding inequality of natural numbers

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

## Reduction

We recall that the rules for reduction of programs are

Define the reduction relation:

## Types

Define a type `Type`

of types for our language.

## Typing

Define the typing relation for the language:

# Properties

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

## Progress

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

# Extensions

## Products

Add products to the language.

## Unit

Add a units to the language.

## Abstractions

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