Ana Bove: Modelling General Recursion in Type Theory

• Based on a practical approach to handling general recursion in type theory.
• Defines a small functional language (called FP), with general recursion.
• Defines a mechanical translation from FP to type theory.
• The method allows for general recursion, including mutual recursion and nested recursion.
• The translated functions look very similar to the original functions.
• Termination proofs are kept apart from the function definitions. This means that
  • You can prove things about functions without first having to prove that they terminate.
  • Partial functions can be handled.
• Non-trivial example: unification.