Inductively Defined Functions in Functional Programming Languages

R. Burstall

Abstract: This paper proposes a notation for defining functions or procedures in such a way that their termination is guaranteed by the scope rules. It uses an extension of case expressions. Suggested uses include programming languages and logical languages; an application is also given to the problem of proving inequalities from initial algebra specifications.

LFCS report ECS-LFCS-87-25

This report was published in Journal of Computer and System Sciences, 34(2/3), pp.409-421.

Previous | Index | Next