Primitive and Some/Any Proof Principles
                for beta-Standardisation

                   Rene Vestergaard
                   

We consider formal provability for three kinds of
beta-standardisation for the lambda-calculus seen as a programming
language and show that there are substantial and instructive
short-comings in the known proofs. In order to overcome the
identified problems, we employ a range of proof techniques that we
have developed for reasoning formally about programming languages,
including "Some/Any proof theory". The techniques are reasonably
mature and succinct and should be of general interest.