next up previous
Next: Introduction

foetus - Termination Checker for Simple Functional Programs

Andreas Abel [*]

July 16, 1998

Abstract:

We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a well-founded structural order on the parameters on the given function to prove termination. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters. The HTML version of this paper contains many ready-to-run Web-based examples.

Run foetus!

Download ML source foetus.tar.gz!



 
next up previous
Next: Introduction
Andreas Abel, 7/16/1998