I design a machine learning system capable of ‘cumulative learning’, which means that it automatically acquires the knowledge necessary for solving harder problems through experience of solving easier ones. Working within the learning framework of inductive programming, I propose that the technique of abstraction, familiar from software engineering, is a suitable mechanism for accumulating knowledge. In abstraction, syntactic patterns in solutions to past problems are isolated as re-usable units and added to background knowledge. For the system’s knowledge representation language, I argue that lambda calculus is a more suitable choice than first-order logic because lambda calculus supports abstraction readily. However, more mature and theoretically well-founded base inference techniques are available within first-order Inductive Logic Programming (ILP). Therefore, my approach is to adapt ILP inference techniques to lambda calculus. Central to ILP is the idea of ‘generality’, and I show that a suitable concept of generality in lambda calculus arises from its standard denotational semantics. Consequently, notions of entailment, subsumption, refinement, and inverse deduction have direct analogues in the lambda calculus setting. I argue that the conventional ‘compression’ measure used in ILP is inflexible in capturing prior assumptions, particularly in the context of an expanding background knowledge. Instead I introduce a non-parametric Bayesian prior over hypotheses and background knowledge. I then design an inductive inference algorithm for the lambda calculus setting based on refinement and proof-directed search. I give a formal proof of correctness of this algorithm. To enable automatic invention of abstractions, I design two algorithms. The first is a heuristic search that uses anti-unification to discovering opportunities for abstraction within a corpus of knowledge. I give a formal characterisation of its search space. The second algorithm performs inverse deduction in order to refactor knowledge in terms of an abstraction. I prove that this refactoring process is semantics-preserving.