Describir: A PROOF-THEORETIC TREATMENT OF λ-REDUCTION WITH CUT-ELIMINATION: λ-CALCULUS AS A LOGIC PROGRAMMING LANGUAGE.