Uniqueness Typing in Natural Deduction Style

A major drawback when developing large applications with functional programming languages is the lack of good debugging tools—when using imperative languages all sorts of useful information about the program’s behaviour is available via a good debugger. In this paper we present a debugging technique that allows the examination of the behaviour of programmer defined functions in the context of the whole program. In particular, we present a technique that allows examination the function input and the result of the application of the function to that input.