Structural Induction and the lambda-Calculus

René Vestergaard

(JAIST - Japan Advanced Institute of Science and Technology, Ishikawa)

Addressing the role of variable binding in higher-order languages presented with simple syntax (in this case, the lambda-calculus), we (i) show that pen-and-paper proofs by structural induction and related proof principles typically, but not always, are formally incomplete rather than incorrect, as would be expected and (ii) account comprehensively for a general proof methodology that serves to bridge the gap between pen-and-paper and formalised proofs by structural proof principles. As well as summarising earlier, formally verified proofs (in Isabelle/HOL) of beta-confluence and the strong weakly-finite beta-development property, we also present formal proofs of eta-confluence, beta,eta-confluence, eta-over-beta-postponement, and notably beta-standardisation. In the latter case, the known proofs fail in rather interesting ways.
Thursday 10th October 2002, 14:00
Robert Recorde Room
Department of Computer Science