Bei funktionalen Programmen spielen zwei Beweisverfahren eine zentrale Rolle:
1. Strukturelle Induktion oder Parameterinduktion
2. Berechnungsinduktion (computational induction) Wir stellen nur die Paramterinduktion/strukturelle Induktion vor.
Bei der Parameterinduktion werden die Eigenschaften einer Funktion für alle Parameter gezeigt, indem man eine Induktion über die Menge der zulässigen Parameter führt.