This thesis presents a compiler from inductive predicates to executable functional equations and a proof procedure to formally verify the compilation in the theorem prover Isabelle/HOL.
This continues the general idea of compiling inductive predicates to functional programs from Berghofer and Nipkow. We adopt their idea of compiling inductive predicates to functions with the use of a mode analysis.
The new contributions are a model for executing inductive predicates in Isabelle/HOL, from which the code generation can create executable code, and a sound and complete proof procedure for the equivalence of the inductive predicate and its functional definition. As a result of this work, we reduce the trusted code base for code generation while still retaining the same functionality.