A semantical analysis of structural recursion
Andreas M. Abel, Thorsten Altenkirch · 2002
dering is wellfounded at each type. A general soundness theorem allows us to conclude that each term accepted by the foetus system actually terminates. Our approach is related to the work by Telford & Turner, who are interested in a total functional programming language (ESFP). In a recent (unpublished) article [TTu98b] they present also a termination analysis based on abstract interpretation. It seems that they accept a larger set of functions but that our analysis of the output of the termination checker is more detailed. Our next goal is to extend our termination checker to coinductively defined types [Coq93, TTu97b] and dependent types, including the definition of universes. We also hope to be able to answer the question whether the restriction of structural recursive function is actually necessary. References