Abstract
This paper discusses the problem of translating a (recursive) function definition expressed in a ML like syntax into a typed A-term. In this paper, we recall how termination proofs can be solutions of the investigated problem. Then we recall how the method of [10] deals with the problem of searching termination proofs. Finally, we discuss the questions raised by the adaptation of our method to the Coq proof assistant.
Cite
CITATION STYLE
Manoury, P. (1995). A user’s friendly syntax to define recursive functions as typed λ-terms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 996, pp. 83–100). Springer Verlag. https://doi.org/10.1007/3-540-60579-7_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
