What are Simple Types (Was: Proofs as programs)

The requirement for week 3 is explicitly lambda expressions:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.
 The logic is the same as in Weekend 2.

For Affine Logic the lambda expressions should have a funny property:
- A variable occurs only once unbound in the bound scope.
For example this here, although it has a simple type:
λ y:A λ x:A->A. x (x y)
It cannot be a proof term of Affine Logic, since x occurs twice.
Some testing showed you don't produce lambda expressions:
You produce:

But I am not familiar with this proof display:
 [
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]

Julio Di Egidio schrieb:

On 18/12/2024 15:30, Mild Shock wrote:
 

Maybe your work qualifies for Weekend 3.

 In fact, I have replied to the WE3 announcement.
 

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

 It implements "affine intuitionistic propositional logic", and I am getting to evaluation/compilation which is the functional side (more details in my initial reply): so, sure, I even classify my reduction rules as intros vs elims...
 What is the deadline?  I don't know what WE is 3.
 -Julio