Comparing integrated and external logics of functional programs

AbstractFour different programming logics are compared by example. Three are versions of Martin-Löf type theory and the fourth is a version of Aczel's logical theory of constructions. They differ in several respects. For example, what is the notion of specification? Are there partial or just total objects? Is general recursion allowed or only primitive recursion of higher type? Is the logic external or integrated? The example is the proof of correctness of a normalization function for conditional expressions