Abstract

I will present a set of editing actions on terms in the simply-typed lambda calculus. These actions preserve the well-typedness of terms, and allow the derivation of any well-typed term beginning with any other well-typed term, without resorting to metavariables or other forms of placeholders. By the time of the talk I hope to have proved that any well-typed term can be constructed from the unit term, and that all editing actions preserve well-typedness.