On Automating the Extraction of Programs from Termination Proofs
Fairouz Kamareddine, François Monin, Maurício Ayala-Rincón · 2003
We investigate an automated program synthesis system that is based on the paradigm of programming by proofs. To automatically extract a #-term that computes a recursive function given by a set of equations the system must find a formal proof of the totality of the given function. Because of the particular logical framework, usually such approaches make it di#cult to use termination techniques such as those in rewriting theory. We overcome this di#culty for the automated system that we consider by exploiting product types. As a consequence, this would enable the incorporation of termination techniques used in other areas while still extracting programs.