List is the most fundamental data type. Is a sequencial argument, is a final sequence of element. It is no possible to have more than one element per box. 
There is two different way to declare a list, the recursive one and the iterative one. 

## Recursive list
- The first box is the **head of the list**
- The rest of the list is **the tail of the list**
- The signature of the recursive list is the following:
```
TYPES
   list, box
     
USES
   element  
   
OPERATIONS
   emptylist : -> list (* Internal operations of list*)
        cons : element x list -> list (* Internal operations of list *)
        tail : list -> list (* Internal operations of list *)
        head : list -> box (* Internal operations of box *)
    contents : box -> element (* Observer of box *)
       first : list ->  element (* Observer of list *)
        next : box -> box (* Internal operation of box *)
        
PRECONDITIONS
   tail(l) is-defined-iaoi l ≠ emptylist
   head(l) is-defined-iaoi l ≠ emptylist
   first(l) is-defined-iaoi l ≠ emptylist  
   
AXIOMS 
   first(_l_) = contents(head(l))
   tail(cons(_e,l_)) = l
   first(cons(_e,l_)) = e
   next(head(_l_)) = head(tail(l)) 
    
WITH 
   list l
   element e
```
`cons` add en element to the head of the list (eg. li <- cons(cloud, li))
`head`return the element in the head of the list (eg. pl <- head(li))
`contents`return what is the element of the head
`first`return the first element of the list (is equivalent to contents)
`tail`remove the first element of the list (eg. fl <- tail (li))
`next`return the element after a box (eg. pspt <= next(head(li))))

## Array implementation
Let's take a list l = E ; D ; C ; B ; A. An array implementation of the list l will be:

|1|2|3|4|5|
|:----:|:----:|:----:|:----:|:----:|
|A|B|C|D|E|
|5|

The first line of the table is the $n^{th}$ place of the element, the second line is all the element of the list, and the third line is the place of the first element of the list (here E is at the $5^{th}$ position).