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